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

Theorem relopabi 5384
Description: A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013.) Remove dependency on ax-sep 4912, ax-nul 4920, ax-pr 5034. (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 4845 . . . . . . . 8 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
31, 2eqtri 2792 . . . . . . 7 𝐴 = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
43abeq2i 2883 . . . . . 6 (𝑧𝐴 ↔ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
5 simpl 468 . . . . . . 7 ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝑧 = ⟨𝑥, 𝑦⟩)
652eximi 1910 . . . . . 6 (∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)
74, 6sylbi 207 . . . . 5 (𝑧𝐴 → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)
8 ax6evr 2099 . . . . . . . . . 10 𝑢 𝑦 = 𝑢
9 pm3.21 448 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ = 𝑧 → (𝑦 = 𝑢 → (𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧)))
109eximdv 1997 . . . . . . . . . 10 (⟨𝑥, 𝑦⟩ = 𝑧 → (∃𝑢 𝑦 = 𝑢 → ∃𝑢(𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧)))
118, 10mpi 20 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ = 𝑧 → ∃𝑢(𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧))
12 opeq2 4538 . . . . . . . . . . 11 (𝑦 = 𝑢 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑢⟩)
13 eqtr2 2790 . . . . . . . . . . . 12 ((⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑢⟩ ∧ ⟨𝑥, 𝑦⟩ = 𝑧) → ⟨𝑥, 𝑢⟩ = 𝑧)
1413eqcomd 2776 . . . . . . . . . . 11 ((⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑢⟩ ∧ ⟨𝑥, 𝑦⟩ = 𝑧) → 𝑧 = ⟨𝑥, 𝑢⟩)
1512, 14sylan 561 . . . . . . . . . 10 ((𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧) → 𝑧 = ⟨𝑥, 𝑢⟩)
1615eximi 1909 . . . . . . . . 9 (∃𝑢(𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧) → ∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
1711, 16syl 17 . . . . . . . 8 (⟨𝑥, 𝑦⟩ = 𝑧 → ∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
1817eqcoms 2778 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
19182eximi 1910 . . . . . 6 (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑥𝑦𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
20 excomim 2198 . . . . . 6 (∃𝑥𝑦𝑢 𝑧 = ⟨𝑥, 𝑢⟩ → ∃𝑦𝑥𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
2119, 20syl 17 . . . . 5 (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑦𝑥𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
22 vex 3352 . . . . . . . . . 10 𝑥 ∈ V
23 vex 3352 . . . . . . . . . 10 𝑢 ∈ V
2422, 23pm3.2i 447 . . . . . . . . 9 (𝑥 ∈ V ∧ 𝑢 ∈ V)
2524jctr 508 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑢⟩ → (𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V)))
26252eximi 1910 . . . . . . 7 (∃𝑥𝑢 𝑧 = ⟨𝑥, 𝑢⟩ → ∃𝑥𝑢(𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V)))
27 df-xp 5255 . . . . . . . . 9 (V × V) = {⟨𝑥, 𝑢⟩ ∣ (𝑥 ∈ V ∧ 𝑢 ∈ V)}
28 df-opab 4845 . . . . . . . . 9 {⟨𝑥, 𝑢⟩ ∣ (𝑥 ∈ V ∧ 𝑢 ∈ V)} = {𝑧 ∣ ∃𝑥𝑢(𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V))}
2927, 28eqtri 2792 . . . . . . . 8 (V × V) = {𝑧 ∣ ∃𝑥𝑢(𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V))}
3029abeq2i 2883 . . . . . . 7 (𝑧 ∈ (V × V) ↔ ∃𝑥𝑢(𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V)))
3126, 30sylibr 224 . . . . . 6 (∃𝑥𝑢 𝑧 = ⟨𝑥, 𝑢⟩ → 𝑧 ∈ (V × V))
3231eximi 1909 . . . . 5 (∃𝑦𝑥𝑢 𝑧 = ⟨𝑥, 𝑢⟩ → ∃𝑦 𝑧 ∈ (V × V))
337, 21, 323syl 18 . . . 4 (𝑧𝐴 → ∃𝑦 𝑧 ∈ (V × V))
34 ax5e 1992 . . . 4 (∃𝑦 𝑧 ∈ (V × V) → 𝑧 ∈ (V × V))
3533, 34syl 17 . . 3 (𝑧𝐴𝑧 ∈ (V × V))
3635ssriv 3754 . 2 𝐴 ⊆ (V × V)
37 df-rel 5256 . 2 (Rel 𝐴𝐴 ⊆ (V × V))
3836, 37mpbir 221 1 Rel 𝐴
Colors of variables: wff setvar class
Syntax hints:  wa 382   = wceq 1630  wex 1851  wcel 2144  {cab 2756  Vcvv 3349  wss 3721  cop 4320  {copab 4844   × cxp 5247  Rel wrel 5254
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-rab 3069  df-v 3351  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-opab 4845  df-xp 5255  df-rel 5256
This theorem is referenced by:  relopab  5386  mptrel  5387  reli  5388  rele  5389  relcnv  5644  cotrg  5648  relco  5777  brfvopabrbr  6421  reloprab  6848  reldmoprab  6891  relrpss  7084  eqer  7930  ecopover  8003  relen  8113  reldom  8114  relfsupp  8432  relwdom  8626  fpwwe2lem2  9655  fpwwe2lem3  9656  fpwwe2lem6  9658  fpwwe2lem7  9659  fpwwe2lem9  9661  fpwwe2lem11  9663  fpwwe2lem12  9664  fpwwe2lem13  9665  fpwwelem  9668  climrel  14430  rlimrel  14431  brstruct  16072  sscrel  16679  gaorber  17947  sylow2a  18240  efgrelexlemb  18369  efgcpbllemb  18374  rellindf  20363  2ndcctbss  21478  refrel  21531  vitalilem1  23595  lgsquadlem1  25325  lgsquadlem2  25326  relsubgr  26383  erclwwlkrel  27164  erclwwlknrel  27221  vcrel  27749  h2hlm  28171  hlimi  28379  relmntop  30402  relae  30637  dmscut  32249  fnerel  32664  filnetlem3  32706  cnfinltrel  33571  brabg2  33835  heiborlem3  33937  heiborlem4  33938  relrngo  34020  isdivrngo  34074  drngoi  34075  isdrngo1  34080  riscer  34112  relcoss  34513  relssr  34585  prter1  34680  prter3  34683  reldvds  39033  nelbrim  41809  rellininds  42750
  Copyright terms: Public domain W3C validator