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

Theorem relopabi 5167
 Description: A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013.) Remove dependency on ax-sep 4709, ax-nul 4717, ax-pr 4833. (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 4644 . . . . . . . 8 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
31, 2eqtri 2632 . . . . . . 7 𝐴 = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
43abeq2i 2722 . . . . . 6 (𝑧𝐴 ↔ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
5 simpl 472 . . . . . . 7 ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝑧 = ⟨𝑥, 𝑦⟩)
652eximi 1753 . . . . . 6 (∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)
74, 6sylbi 206 . . . . 5 (𝑧𝐴 → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)
8 ax6evr 1929 . . . . . . . . . 10 𝑢 𝑦 = 𝑢
9 pm3.21 463 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ = 𝑧 → (𝑦 = 𝑢 → (𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧)))
109eximdv 1833 . . . . . . . . . 10 (⟨𝑥, 𝑦⟩ = 𝑧 → (∃𝑢 𝑦 = 𝑢 → ∃𝑢(𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧)))
118, 10mpi 20 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ = 𝑧 → ∃𝑢(𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧))
12 opeq2 4341 . . . . . . . . . . 11 (𝑦 = 𝑢 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑢⟩)
13 eqtr2 2630 . . . . . . . . . . . 12 ((⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑢⟩ ∧ ⟨𝑥, 𝑦⟩ = 𝑧) → ⟨𝑥, 𝑢⟩ = 𝑧)
1413eqcomd 2616 . . . . . . . . . . 11 ((⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑢⟩ ∧ ⟨𝑥, 𝑦⟩ = 𝑧) → 𝑧 = ⟨𝑥, 𝑢⟩)
1512, 14sylan 487 . . . . . . . . . 10 ((𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧) → 𝑧 = ⟨𝑥, 𝑢⟩)
1615eximi 1752 . . . . . . . . 9 (∃𝑢(𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧) → ∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
1711, 16syl 17 . . . . . . . 8 (⟨𝑥, 𝑦⟩ = 𝑧 → ∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
1817eqcoms 2618 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
19182eximi 1753 . . . . . 6 (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑥𝑦𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
20 excomim 2030 . . . . . 6 (∃𝑥𝑦𝑢 𝑧 = ⟨𝑥, 𝑢⟩ → ∃𝑦𝑥𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
2119, 20syl 17 . . . . 5 (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑦𝑥𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
22 vex 3176 . . . . . . . . . 10 𝑥 ∈ V
23 vex 3176 . . . . . . . . . 10 𝑢 ∈ V
2422, 23pm3.2i 470 . . . . . . . . 9 (𝑥 ∈ V ∧ 𝑢 ∈ V)
2524jctr 563 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑢⟩ → (𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V)))
26252eximi 1753 . . . . . . 7 (∃𝑥𝑢 𝑧 = ⟨𝑥, 𝑢⟩ → ∃𝑥𝑢(𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V)))
27 df-xp 5044 . . . . . . . . 9 (V × V) = {⟨𝑥, 𝑢⟩ ∣ (𝑥 ∈ V ∧ 𝑢 ∈ V)}
28 df-opab 4644 . . . . . . . . 9 {⟨𝑥, 𝑢⟩ ∣ (𝑥 ∈ V ∧ 𝑢 ∈ V)} = {𝑧 ∣ ∃𝑥𝑢(𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V))}
2927, 28eqtri 2632 . . . . . . . 8 (V × V) = {𝑧 ∣ ∃𝑥𝑢(𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V))}
3029abeq2i 2722 . . . . . . 7 (𝑧 ∈ (V × V) ↔ ∃𝑥𝑢(𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V)))
3126, 30sylibr 223 . . . . . 6 (∃𝑥𝑢 𝑧 = ⟨𝑥, 𝑢⟩ → 𝑧 ∈ (V × V))
3231eximi 1752 . . . . 5 (∃𝑦𝑥𝑢 𝑧 = ⟨𝑥, 𝑢⟩ → ∃𝑦 𝑧 ∈ (V × V))
337, 21, 323syl 18 . . . 4 (𝑧𝐴 → ∃𝑦 𝑧 ∈ (V × V))
34 ax5e 1829 . . . 4 (∃𝑦 𝑧 ∈ (V × V) → 𝑧 ∈ (V × V))
3533, 34syl 17 . . 3 (𝑧𝐴𝑧 ∈ (V × V))
3635ssriv 3572 . 2 𝐴 ⊆ (V × V)
37 df-rel 5045 . 2 (Rel 𝐴𝐴 ⊆ (V × V))
3836, 37mpbir 220 1 Rel 𝐴
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {cab 2596  Vcvv 3173   ⊆ wss 3540  ⟨cop 4131  {copab 4642   × cxp 5036  Rel wrel 5043 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-opab 4644  df-xp 5044  df-rel 5045 This theorem is referenced by:  relopab  5169  mptrel  5170  reli  5171  rele  5172  relcnv  5422  cotrg  5426  relco  5550  reloprab  6600  reldmoprab  6643  relrpss  6836  eqer  7664  eqerOLD  7665  ecopover  7738  ecopoverOLD  7739  relen  7846  reldom  7847  relfsupp  8160  relwdom  8354  fpwwe2lem2  9333  fpwwe2lem3  9334  fpwwe2lem6  9336  fpwwe2lem7  9337  fpwwe2lem9  9339  fpwwe2lem11  9341  fpwwe2lem12  9342  fpwwe2lem13  9343  fpwwelem  9346  climrel  14071  rlimrel  14072  brstruct  15703  sscrel  16296  gaorber  17564  sylow2a  17857  efgrelexlemb  17986  efgcpbllemb  17991  rellindf  19966  2ndcctbss  21068  refrel  21121  vitalilem1  23182  vitalilem1OLD  23183  lgsquadlem1  24905  lgsquadlem2  24906  reluhgra  25823  relushgra  25824  relumgra  25843  reluslgra  25863  relusgra  25864  iscusgra0  25986  cusgrasize  26006  erclwwlkrel  26338  erclwwlknrel  26350  frisusgrapr  26518  vcrel  26799  h2hlm  27221  hlimi  27429  relmntop  29396  relae  29630  fnerel  31503  filnetlem3  31545  brabg2  32680  heiborlem3  32782  heiborlem4  32783  relrngo  32865  isdivrngo  32919  drngoi  32920  isdrngo1  32925  riscer  32957  prter1  33182  prter3  33185  reldvds  37536  relsubgr  40493  erclwwlksrel  41238  erclwwlksnrel  41250  rellininds  42026
 Copyright terms: Public domain W3C validator