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

Theorem relopabi 5541
Description: A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013.) Remove dependency on ax-sep 5058, ax-nul 5065, ax-pr 5184. (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 4990 . . . . . . . 8 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
31, 2eqtri 2799 . . . . . . 7 𝐴 = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
43abeq2i 2897 . . . . . 6 (𝑧𝐴 ↔ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
5 simpl 475 . . . . . . 7 ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝑧 = ⟨𝑥, 𝑦⟩)
652eximi 1798 . . . . . 6 (∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)
74, 6sylbi 209 . . . . 5 (𝑧𝐴 → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)
8 ax6evr 1971 . . . . . . . . . 10 𝑢 𝑦 = 𝑢
9 pm3.21 464 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ = 𝑧 → (𝑦 = 𝑢 → (𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧)))
109eximdv 1876 . . . . . . . . . 10 (⟨𝑥, 𝑦⟩ = 𝑧 → (∃𝑢 𝑦 = 𝑢 → ∃𝑢(𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧)))
118, 10mpi 20 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ = 𝑧 → ∃𝑢(𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧))
12 opeq2 4676 . . . . . . . . . . 11 (𝑦 = 𝑢 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑢⟩)
13 eqtr2 2797 . . . . . . . . . . . 12 ((⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑢⟩ ∧ ⟨𝑥, 𝑦⟩ = 𝑧) → ⟨𝑥, 𝑢⟩ = 𝑧)
1413eqcomd 2781 . . . . . . . . . . 11 ((⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑢⟩ ∧ ⟨𝑥, 𝑦⟩ = 𝑧) → 𝑧 = ⟨𝑥, 𝑢⟩)
1512, 14sylan 572 . . . . . . . . . 10 ((𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧) → 𝑧 = ⟨𝑥, 𝑢⟩)
1615eximi 1797 . . . . . . . . 9 (∃𝑢(𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧) → ∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
1711, 16syl 17 . . . . . . . 8 (⟨𝑥, 𝑦⟩ = 𝑧 → ∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
1817eqcoms 2783 . . . . . . 7 (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
19182eximi 1798 . . . . . 6 (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑥𝑦𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
20 excomim 2097 . . . . . 6 (∃𝑥𝑦𝑢 𝑧 = ⟨𝑥, 𝑢⟩ → ∃𝑦𝑥𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
2119, 20syl 17 . . . . 5 (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑦𝑥𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
22 vex 3415 . . . . . . . . . 10 𝑥 ∈ V
23 vex 3415 . . . . . . . . . 10 𝑢 ∈ V
2422, 23pm3.2i 463 . . . . . . . . 9 (𝑥 ∈ V ∧ 𝑢 ∈ V)
2524jctr 517 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑢⟩ → (𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V)))
26252eximi 1798 . . . . . . 7 (∃𝑥𝑢 𝑧 = ⟨𝑥, 𝑢⟩ → ∃𝑥𝑢(𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V)))
27 df-xp 5410 . . . . . . . . 9 (V × V) = {⟨𝑥, 𝑢⟩ ∣ (𝑥 ∈ V ∧ 𝑢 ∈ V)}
28 df-opab 4990 . . . . . . . . 9 {⟨𝑥, 𝑢⟩ ∣ (𝑥 ∈ V ∧ 𝑢 ∈ V)} = {𝑧 ∣ ∃𝑥𝑢(𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V))}
2927, 28eqtri 2799 . . . . . . . 8 (V × V) = {𝑧 ∣ ∃𝑥𝑢(𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V))}
3029abeq2i 2897 . . . . . . 7 (𝑧 ∈ (V × V) ↔ ∃𝑥𝑢(𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V)))
3126, 30sylibr 226 . . . . . 6 (∃𝑥𝑢 𝑧 = ⟨𝑥, 𝑢⟩ → 𝑧 ∈ (V × V))
3231eximi 1797 . . . . 5 (∃𝑦𝑥𝑢 𝑧 = ⟨𝑥, 𝑢⟩ → ∃𝑦 𝑧 ∈ (V × V))
337, 21, 323syl 18 . . . 4 (𝑧𝐴 → ∃𝑦 𝑧 ∈ (V × V))
34 ax5e 1871 . . . 4 (∃𝑦 𝑧 ∈ (V × V) → 𝑧 ∈ (V × V))
3533, 34syl 17 . . 3 (𝑧𝐴𝑧 ∈ (V × V))
3635ssriv 3861 . 2 𝐴 ⊆ (V × V)
37 df-rel 5411 . 2 (Rel 𝐴𝐴 ⊆ (V × V))
3836, 37mpbir 223 1 Rel 𝐴
Colors of variables: wff setvar class
Syntax hints:  wa 387   = wceq 1507  wex 1742  wcel 2048  {cab 2755  Vcvv 3412  wss 3828  cop 4445  {copab 4989   × cxp 5402  Rel wrel 5409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2747
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-rab 3094  df-v 3414  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-nul 4178  df-if 4349  df-sn 4440  df-pr 4442  df-op 4446  df-opab 4990  df-xp 5410  df-rel 5411
This theorem is referenced by:  relopab  5543  mptrel  5544  reli  5545  rele  5546  relcnv  5805  cotrg  5809  relco  5934  brfvopabrbr  6590  reloprab  7030  reldmoprab  7073  relrpss  7266  eqer  8120  ecopover  8197  relen  8307  reldom  8308  relfsupp  8626  relwdom  8821  fpwwe2lem2  9848  fpwwe2lem3  9849  fpwwe2lem6  9851  fpwwe2lem7  9852  fpwwe2lem9  9854  fpwwe2lem11  9856  fpwwe2lem12  9857  fpwwe2lem13  9858  fpwwelem  9861  climrel  14704  rlimrel  14705  brstruct  16342  sscrel  16935  gaorber  18203  sylow2a  18499  efgrelexlemb  18630  efgcpbllemb  18635  rellindf  20648  2ndcctbss  21761  refrel  21814  vitalilem1  23906  lgsquadlem1  25652  lgsquadlem2  25653  relsubgr  26748  erclwwlkrel  27526  erclwwlknrel  27584  vcrel  28108  h2hlm  28530  hlimi  28738  relmntop  30900  relae  31135  dmscut  32763  fnerel  33177  filnetlem3  33219  brabg2  34411  heiborlem3  34511  heiborlem4  34512  relrngo  34594  isdivrngo  34648  drngoi  34649  isdrngo1  34654  riscer  34686  relcoss  35091  relssr  35163  prter1  35438  prter3  35441  prjsper  38643  reldvds  40040  nelbrim  42859  isomgrrel  43329  rellininds  43839
  Copyright terms: Public domain W3C validator