MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  relopabi Structured version   Visualization version   GIF version

Theorem relopabi 5234
Description: A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013.) Remove dependency on ax-sep 4772, ax-nul 4780, ax-pr 4897. (Revised by KP, 25-Oct-2021.)
Hypothesis
Ref Expression
relopabi.1 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
Assertion
Ref Expression
relopabi Rel 𝐴

Proof of Theorem relopabi
Dummy variables 𝑧 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relopabi.1 . . . . . . . 8 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
2 df-opab 4704 . . . . . . . 8 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
31, 2eqtri 2642 . . . . . . 7 𝐴 = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
43abeq2i 2733 . . . . . 6 (𝑧𝐴 ↔ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
5 simpl 473 . . . . . . 7 ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝑧 = ⟨𝑥, 𝑦⟩)
652eximi 1761 . . . . . 6 (∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)
74, 6sylbi 207 . . . . 5 (𝑧𝐴 → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)
8 ax6evr 1940 . . . . . . . . . 10 𝑢 𝑦 = 𝑢
9 pm3.21 464 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ = 𝑧 → (𝑦 = 𝑢 → (𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧)))
109eximdv 1844 . . . . . . . . . 10 (⟨𝑥, 𝑦⟩ = 𝑧 → (∃𝑢 𝑦 = 𝑢 → ∃𝑢(𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧)))
118, 10mpi 20 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ = 𝑧 → ∃𝑢(𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧))
12 opeq2 4394 . . . . . . . . . . 11 (𝑦 = 𝑢 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑢⟩)
13 eqtr2 2640 . . . . . . . . . . . 12 ((⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑢⟩ ∧ ⟨𝑥, 𝑦⟩ = 𝑧) → ⟨𝑥, 𝑢⟩ = 𝑧)
1413eqcomd 2626 . . . . . . . . . . 11 ((⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑢⟩ ∧ ⟨𝑥, 𝑦⟩ = 𝑧) → 𝑧 = ⟨𝑥, 𝑢⟩)
1512, 14sylan 488 . . . . . . . . . 10 ((𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧) → 𝑧 = ⟨𝑥, 𝑢⟩)
1615eximi 1760 . . . . . . . . 9 (∃𝑢(𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧) → ∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
1711, 16syl 17 . . . . . . . 8 (⟨𝑥, 𝑦⟩ = 𝑧 → ∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
1817eqcoms 2628 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
19182eximi 1761 . . . . . 6 (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑥𝑦𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
20 excomim 2041 . . . . . 6 (∃𝑥𝑦𝑢 𝑧 = ⟨𝑥, 𝑢⟩ → ∃𝑦𝑥𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
2119, 20syl 17 . . . . 5 (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑦𝑥𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
22 vex 3198 . . . . . . . . . 10 𝑥 ∈ V
23 vex 3198 . . . . . . . . . 10 𝑢 ∈ V
2422, 23pm3.2i 471 . . . . . . . . 9 (𝑥 ∈ V ∧ 𝑢 ∈ V)
2524jctr 564 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑢⟩ → (𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V)))
26252eximi 1761 . . . . . . 7 (∃𝑥𝑢 𝑧 = ⟨𝑥, 𝑢⟩ → ∃𝑥𝑢(𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V)))
27 df-xp 5110 . . . . . . . . 9 (V × V) = {⟨𝑥, 𝑢⟩ ∣ (𝑥 ∈ V ∧ 𝑢 ∈ V)}
28 df-opab 4704 . . . . . . . . 9 {⟨𝑥, 𝑢⟩ ∣ (𝑥 ∈ V ∧ 𝑢 ∈ V)} = {𝑧 ∣ ∃𝑥𝑢(𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V))}
2927, 28eqtri 2642 . . . . . . . 8 (V × V) = {𝑧 ∣ ∃𝑥𝑢(𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V))}
3029abeq2i 2733 . . . . . . 7 (𝑧 ∈ (V × V) ↔ ∃𝑥𝑢(𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V)))
3126, 30sylibr 224 . . . . . 6 (∃𝑥𝑢 𝑧 = ⟨𝑥, 𝑢⟩ → 𝑧 ∈ (V × V))
3231eximi 1760 . . . . 5 (∃𝑦𝑥𝑢 𝑧 = ⟨𝑥, 𝑢⟩ → ∃𝑦 𝑧 ∈ (V × V))
337, 21, 323syl 18 . . . 4 (𝑧𝐴 → ∃𝑦 𝑧 ∈ (V × V))
34 ax5e 1839 . . . 4 (∃𝑦 𝑧 ∈ (V × V) → 𝑧 ∈ (V × V))
3533, 34syl 17 . . 3 (𝑧𝐴𝑧 ∈ (V × V))
3635ssriv 3599 . 2 𝐴 ⊆ (V × V)
37 df-rel 5111 . 2 (Rel 𝐴𝐴 ⊆ (V × V))
3836, 37mpbir 221 1 Rel 𝐴
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1481  wex 1702  wcel 1988  {cab 2606  Vcvv 3195  wss 3567  cop 4174  {copab 4703   × cxp 5102  Rel wrel 5109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-opab 4704  df-xp 5110  df-rel 5111
This theorem is referenced by:  relopab  5236  mptrel  5237  reli  5238  rele  5239  relcnv  5491  cotrg  5495  relco  5621  brfvopabrbr  6266  reloprab  6687  reldmoprab  6730  relrpss  6923  eqer  7762  eqerOLD  7763  ecopover  7836  ecopoverOLD  7837  relen  7945  reldom  7946  relfsupp  8262  relwdom  8456  fpwwe2lem2  9439  fpwwe2lem3  9440  fpwwe2lem6  9442  fpwwe2lem7  9443  fpwwe2lem9  9445  fpwwe2lem11  9447  fpwwe2lem12  9448  fpwwe2lem13  9449  fpwwelem  9452  climrel  14204  rlimrel  14205  brstruct  15847  sscrel  16454  gaorber  17722  sylow2a  18015  efgrelexlemb  18144  efgcpbllemb  18149  rellindf  20128  2ndcctbss  21239  refrel  21292  vitalilem1  23357  vitalilem1OLD  23358  lgsquadlem1  25086  lgsquadlem2  25087  relsubgr  26142  erclwwlksrel  26911  erclwwlksnrel  26923  vcrel  27385  h2hlm  27807  hlimi  28015  relmntop  30042  relae  30277  dmscut  31892  fnerel  32308  filnetlem3  32350  brabg2  33481  heiborlem3  33583  heiborlem4  33584  relrngo  33666  isdivrngo  33720  drngoi  33721  isdrngo1  33726  riscer  33758  prter1  33983  prter3  33986  reldvds  38334  nelbrim  41055  rellininds  41997
  Copyright terms: Public domain W3C validator