Theorem relopabi

Description: A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013) Remove dependency on ax-sep , ax-nul , ax-pr . (Revised by KP, 25-Oct-2021)

	Ref	Expression
Hypothesis	relopabi.1	⊢ 𝐴 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
Assertion	relopabi	⊢ Rel 𝐴

Proof

Step	Hyp	Ref	Expression
1		relopabi.1	⊢ 𝐴 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
2		df-opab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }
3	1 2	eqtri	⊢ 𝐴 = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }
4	3	abeq2i	⊢ ( 𝑧 ∈ 𝐴 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
5		simpl	⊢ ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
6	5	2eximi	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
7	4 6	sylbi	⊢ ( 𝑧 ∈ 𝐴 → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
8		ax6evr	⊢ ∃ 𝑢 𝑦 = 𝑢
9		pm3.21	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = 𝑧 → ( 𝑦 = 𝑢 → ( 𝑦 = 𝑢 ∧ ⟨ 𝑥 , 𝑦 ⟩ = 𝑧 ) ) )
10	9	eximdv	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = 𝑧 → ( ∃ 𝑢 𝑦 = 𝑢 → ∃ 𝑢 ( 𝑦 = 𝑢 ∧ ⟨ 𝑥 , 𝑦 ⟩ = 𝑧 ) ) )
11	8 10	mpi	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = 𝑧 → ∃ 𝑢 ( 𝑦 = 𝑢 ∧ ⟨ 𝑥 , 𝑦 ⟩ = 𝑧 ) )
12		opeq2	⊢ ( 𝑦 = 𝑢 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑢 ⟩ )
13		eqtr2	⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑢 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ = 𝑧 ) → ⟨ 𝑥 , 𝑢 ⟩ = 𝑧 )
14	13	eqcomd	⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑢 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ = 𝑧 ) → 𝑧 = ⟨ 𝑥 , 𝑢 ⟩ )
15	12 14	sylan	⊢ ( ( 𝑦 = 𝑢 ∧ ⟨ 𝑥 , 𝑦 ⟩ = 𝑧 ) → 𝑧 = ⟨ 𝑥 , 𝑢 ⟩ )
16	15	eximi	⊢ ( ∃ 𝑢 ( 𝑦 = 𝑢 ∧ ⟨ 𝑥 , 𝑦 ⟩ = 𝑧 ) → ∃ 𝑢 𝑧 = ⟨ 𝑥 , 𝑢 ⟩ )
17	11 16	syl	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = 𝑧 → ∃ 𝑢 𝑧 = ⟨ 𝑥 , 𝑢 ⟩ )
18	17	eqcoms	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑢 𝑧 = ⟨ 𝑥 , 𝑢 ⟩ )
19	18	2eximi	⊢ ( ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑥 ∃ 𝑦 ∃ 𝑢 𝑧 = ⟨ 𝑥 , 𝑢 ⟩ )
20		excomim	⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑢 𝑧 = ⟨ 𝑥 , 𝑢 ⟩ → ∃ 𝑦 ∃ 𝑥 ∃ 𝑢 𝑧 = ⟨ 𝑥 , 𝑢 ⟩ )
21	19 20	syl	⊢ ( ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑦 ∃ 𝑥 ∃ 𝑢 𝑧 = ⟨ 𝑥 , 𝑢 ⟩ )
22		vex	⊢ 𝑥 ∈ V
23		vex	⊢ 𝑢 ∈ V
24	22 23	pm3.2i	⊢ ( 𝑥 ∈ V ∧ 𝑢 ∈ V )
25	24	jctr	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑢 ⟩ → ( 𝑧 = ⟨ 𝑥 , 𝑢 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑢 ∈ V ) ) )
26	25	2eximi	⊢ ( ∃ 𝑥 ∃ 𝑢 𝑧 = ⟨ 𝑥 , 𝑢 ⟩ → ∃ 𝑥 ∃ 𝑢 ( 𝑧 = ⟨ 𝑥 , 𝑢 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑢 ∈ V ) ) )
27		df-xp	⊢ ( V × V ) = { ⟨ 𝑥 , 𝑢 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑢 ∈ V ) }
28		df-opab	⊢ { ⟨ 𝑥 , 𝑢 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑢 ∈ V ) } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑢 ( 𝑧 = ⟨ 𝑥 , 𝑢 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑢 ∈ V ) ) }
29	27 28	eqtri	⊢ ( V × V ) = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑢 ( 𝑧 = ⟨ 𝑥 , 𝑢 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑢 ∈ V ) ) }
30	29	abeq2i	⊢ ( 𝑧 ∈ ( V × V ) ↔ ∃ 𝑥 ∃ 𝑢 ( 𝑧 = ⟨ 𝑥 , 𝑢 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑢 ∈ V ) ) )
31	26 30	sylibr	⊢ ( ∃ 𝑥 ∃ 𝑢 𝑧 = ⟨ 𝑥 , 𝑢 ⟩ → 𝑧 ∈ ( V × V ) )
32	31	eximi	⊢ ( ∃ 𝑦 ∃ 𝑥 ∃ 𝑢 𝑧 = ⟨ 𝑥 , 𝑢 ⟩ → ∃ 𝑦 𝑧 ∈ ( V × V ) )
33	7 21 32	3syl	⊢ ( 𝑧 ∈ 𝐴 → ∃ 𝑦 𝑧 ∈ ( V × V ) )
34		ax5e	⊢ ( ∃ 𝑦 𝑧 ∈ ( V × V ) → 𝑧 ∈ ( V × V ) )
35	33 34	syl	⊢ ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ( V × V ) )
36	35	ssriv	⊢ 𝐴 ⊆ ( V × V )
37		df-rel	⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( V × V ) )
38	36 37	mpbir	⊢ Rel 𝐴