Theorem relopabi 5658

Description: A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013.) Remove dependency on ax-sep 5167, ax-nul 5174, ax-pr 5295. (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.

Step	Hyp	Ref	Expression
1		relopabi.1	. . . . . . . 8 ⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
2		df-opab 5093	. . . . . . . 8 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
3	1, 2	eqtri 2821	. . . . . . 7 ⊢ 𝐴 = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
4	3	abeq2i 2925	. . . . . 6 ⊢ (𝑧 ∈ 𝐴 ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
5		simpl 486	. . . . . . 7 ⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝑧 = ⟨𝑥, 𝑦⟩)
6	5	2eximi 1837	. . . . . 6 ⊢ (∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩)
7	4, 6	sylbi 220	. . . . 5 ⊢ (𝑧 ∈ 𝐴 → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩)
8		ax6evr 2022	. . . . . . . . . 10 ⊢ ∃𝑢 𝑦 = 𝑢
9		pm3.21 475	. . . . . . . . . . 11 ⊢ (⟨𝑥, 𝑦⟩ = 𝑧 → (𝑦 = 𝑢 → (𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧)))
10	9	eximdv 1918	. . . . . . . . . 10 ⊢ (⟨𝑥, 𝑦⟩ = 𝑧 → (∃𝑢 𝑦 = 𝑢 → ∃𝑢(𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧)))
11	8, 10	mpi 20	. . . . . . . . 9 ⊢ (⟨𝑥, 𝑦⟩ = 𝑧 → ∃𝑢(𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧))
12		opeq2 4765	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑢 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑢⟩)
13		eqtr2 2819	. . . . . . . . . . . 12 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑢⟩ ∧ ⟨𝑥, 𝑦⟩ = 𝑧) → ⟨𝑥, 𝑢⟩ = 𝑧)
14	13	eqcomd 2804	. . . . . . . . . . 11 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑢⟩ ∧ ⟨𝑥, 𝑦⟩ = 𝑧) → 𝑧 = ⟨𝑥, 𝑢⟩)
15	12, 14	sylan 583	. . . . . . . . . 10 ⊢ ((𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧) → 𝑧 = ⟨𝑥, 𝑢⟩)
16	15	eximi 1836	. . . . . . . . 9 ⊢ (∃𝑢(𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧) → ∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
17	11, 16	syl 17	. . . . . . . 8 ⊢ (⟨𝑥, 𝑦⟩ = 𝑧 → ∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
18	17	eqcoms 2806	. . . . . . 7 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
19	18	2eximi 1837	. . . . . 6 ⊢ (∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑥∃𝑦∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
20		excomim 2167	. . . . . 6 ⊢ (∃𝑥∃𝑦∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩ → ∃𝑦∃𝑥∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
21	19, 20	syl 17	. . . . 5 ⊢ (∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑦∃𝑥∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩)
22		vex 3444	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
23		vex 3444	. . . . . . . . . 10 ⊢ 𝑢 ∈ V
24	22, 23	pm3.2i 474	. . . . . . . . 9 ⊢ (𝑥 ∈ V ∧ 𝑢 ∈ V)
25	24	jctr 528	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑥, 𝑢⟩ → (𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V)))
26	25	2eximi 1837	. . . . . . 7 ⊢ (∃𝑥∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩ → ∃𝑥∃𝑢(𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V)))
27		df-xp 5525	. . . . . . . . 9 ⊢ (V × V) = {⟨𝑥, 𝑢⟩ ∣ (𝑥 ∈ V ∧ 𝑢 ∈ V)}
28		df-opab 5093	. . . . . . . . 9 ⊢ {⟨𝑥, 𝑢⟩ ∣ (𝑥 ∈ V ∧ 𝑢 ∈ V)} = {𝑧 ∣ ∃𝑥∃𝑢(𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V))}
29	27, 28	eqtri 2821	. . . . . . . 8 ⊢ (V × V) = {𝑧 ∣ ∃𝑥∃𝑢(𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V))}
30	29	abeq2i 2925	. . . . . . 7 ⊢ (𝑧 ∈ (V × V) ↔ ∃𝑥∃𝑢(𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V)))
31	26, 30	sylibr 237	. . . . . 6 ⊢ (∃𝑥∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩ → 𝑧 ∈ (V × V))
32	31	eximi 1836	. . . . 5 ⊢ (∃𝑦∃𝑥∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩ → ∃𝑦 𝑧 ∈ (V × V))
33	7, 21, 32	3syl 18	. . . 4 ⊢ (𝑧 ∈ 𝐴 → ∃𝑦 𝑧 ∈ (V × V))
34		ax5e 1913	. . . 4 ⊢ (∃𝑦 𝑧 ∈ (V × V) → 𝑧 ∈ (V × V))
35	33, 34	syl 17	. . 3 ⊢ (𝑧 ∈ 𝐴 → 𝑧 ∈ (V × V))
36	35	ssriv 3919	. 2 ⊢ 𝐴 ⊆ (V × V)
37		df-rel 5526	. 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
38	36, 37	mpbir 234	1 ⊢ Rel 𝐴

Syntax hints:   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  {cab 2776  Vcvv 3441   ⊆ wss 3881  ⟨cop 4531  {copab 5092   × cxp 5517  Rel wrel 5524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-opab 5093  df-xp 5525  df-rel 5526

This theorem is referenced by:  relopab  5660  mptrel  5661  reli  5662  rele  5663  relcnv  5934  cotrg  5938  relco  6064  brfvopabrbr  6742  reloprab  7192  reldmoprab  7238  relrpss  7430  eqer  8307  ecopover  8384  relen  8497  reldom  8498  relfsupp  8819  relwdom  9014  fpwwe2lem2  10043  fpwwe2lem3  10044  fpwwe2lem6  10046  fpwwe2lem7  10047  fpwwe2lem9  10049  fpwwe2lem11  10051  fpwwe2lem12  10052  fpwwe2lem13  10053  fpwwelem  10056  climrel  14841  rlimrel  14842  brstruct  16484  sscrel  17075  gaorber  18430  sylow2a  18736  efgrelexlemb  18868  efgcpbllemb  18873  rellindf  20497  2ndcctbss  22060  refrel  22113  vitalilem1  24212  lgsquadlem1  25964  lgsquadlem2  25965  relsubgr  27059  erclwwlkrel  27802  erclwwlknrel  27851  vcrel  28343  h2hlm  28763  hlimi  28971  relmntop  31375  relae  31609  dmscut  33385  fnerel  33799  filnetlem3  33841  brabg2  35154  heiborlem3  35251  heiborlem4  35252  relrngo  35334  isdivrngo  35388  drngoi  35389  isdrngo1  35394  riscer  35426  relcoss  35828  relssr  35900  prter1  36175  prter3  36178  prjsper  39602  reldvds  41019  nelbrim  43831  isomgrrel  44340  rellininds  44852