Theorem opabex3d

Description: Existence of an ordered pair abstraction, deduction version. (Contributed by Alexander van der Vekens, 19-Oct-2017)

	Ref	Expression
Hypotheses	opabex3d.1	⊢ ( 𝜑 → 𝐴 ∈ V )
	opabex3d.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → { 𝑦 ∣ 𝜓 } ∈ V )
Assertion	opabex3d	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		opabex3d.1	⊢ ( 𝜑 → 𝐴 ∈ V )
2		opabex3d.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → { 𝑦 ∣ 𝜓 } ∈ V )
3		19.42v	⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) )
4		an12	⊢ ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) )
5	4	exbii	⊢ ( ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) )
6		elxp	⊢ ( 𝑧 ∈ ( { 𝑥 } × { 𝑦 ∣ 𝜓 } ) ↔ ∃ 𝑣 ∃ 𝑤 ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ ( 𝑣 ∈ { 𝑥 } ∧ 𝑤 ∈ { 𝑦 ∣ 𝜓 } ) ) )
7		excom	⊢ ( ∃ 𝑣 ∃ 𝑤 ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ ( 𝑣 ∈ { 𝑥 } ∧ 𝑤 ∈ { 𝑦 ∣ 𝜓 } ) ) ↔ ∃ 𝑤 ∃ 𝑣 ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ ( 𝑣 ∈ { 𝑥 } ∧ 𝑤 ∈ { 𝑦 ∣ 𝜓 } ) ) )
8		an12	⊢ ( ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ ( 𝑣 ∈ { 𝑥 } ∧ 𝑤 ∈ { 𝑦 ∣ 𝜓 } ) ) ↔ ( 𝑣 ∈ { 𝑥 } ∧ ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦 ∣ 𝜓 } ) ) )
9		velsn	⊢ ( 𝑣 ∈ { 𝑥 } ↔ 𝑣 = 𝑥 )
10	9	anbi1i	⊢ ( ( 𝑣 ∈ { 𝑥 } ∧ ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦 ∣ 𝜓 } ) ) ↔ ( 𝑣 = 𝑥 ∧ ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦 ∣ 𝜓 } ) ) )
11	8 10	bitri	⊢ ( ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ ( 𝑣 ∈ { 𝑥 } ∧ 𝑤 ∈ { 𝑦 ∣ 𝜓 } ) ) ↔ ( 𝑣 = 𝑥 ∧ ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦 ∣ 𝜓 } ) ) )
12	11	exbii	⊢ ( ∃ 𝑣 ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ ( 𝑣 ∈ { 𝑥 } ∧ 𝑤 ∈ { 𝑦 ∣ 𝜓 } ) ) ↔ ∃ 𝑣 ( 𝑣 = 𝑥 ∧ ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦 ∣ 𝜓 } ) ) )
13		opeq1	⊢ ( 𝑣 = 𝑥 → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑤 ⟩ )
14	13	eqeq2d	⊢ ( 𝑣 = 𝑥 → ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ↔ 𝑧 = ⟨ 𝑥 , 𝑤 ⟩ ) )
15	14	anbi1d	⊢ ( 𝑣 = 𝑥 → ( ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦 ∣ 𝜓 } ) ↔ ( 𝑧 = ⟨ 𝑥 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦 ∣ 𝜓 } ) ) )
16	15	equsexvw	⊢ ( ∃ 𝑣 ( 𝑣 = 𝑥 ∧ ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦 ∣ 𝜓 } ) ) ↔ ( 𝑧 = ⟨ 𝑥 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦 ∣ 𝜓 } ) )
17	12 16	bitri	⊢ ( ∃ 𝑣 ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ ( 𝑣 ∈ { 𝑥 } ∧ 𝑤 ∈ { 𝑦 ∣ 𝜓 } ) ) ↔ ( 𝑧 = ⟨ 𝑥 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦 ∣ 𝜓 } ) )
18	17	exbii	⊢ ( ∃ 𝑤 ∃ 𝑣 ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ ( 𝑣 ∈ { 𝑥 } ∧ 𝑤 ∈ { 𝑦 ∣ 𝜓 } ) ) ↔ ∃ 𝑤 ( 𝑧 = ⟨ 𝑥 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦 ∣ 𝜓 } ) )
19	7 18	bitri	⊢ ( ∃ 𝑣 ∃ 𝑤 ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ ∧ ( 𝑣 ∈ { 𝑥 } ∧ 𝑤 ∈ { 𝑦 ∣ 𝜓 } ) ) ↔ ∃ 𝑤 ( 𝑧 = ⟨ 𝑥 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦 ∣ 𝜓 } ) )
20		nfv	⊢ Ⅎ 𝑦 𝑧 = ⟨ 𝑥 , 𝑤 ⟩
21		nfsab1	⊢ Ⅎ 𝑦 𝑤 ∈ { 𝑦 ∣ 𝜓 }
22	20 21	nfan	⊢ Ⅎ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦 ∣ 𝜓 } )
23		nfv	⊢ Ⅎ 𝑤 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 )
24		opeq2	⊢ ( 𝑤 = 𝑦 → ⟨ 𝑥 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
25	24	eqeq2d	⊢ ( 𝑤 = 𝑦 → ( 𝑧 = ⟨ 𝑥 , 𝑤 ⟩ ↔ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) )
26		sbequ12	⊢ ( 𝑦 = 𝑤 → ( 𝜓 ↔ [ 𝑤 / 𝑦 ] 𝜓 ) )
27	26	equcoms	⊢ ( 𝑤 = 𝑦 → ( 𝜓 ↔ [ 𝑤 / 𝑦 ] 𝜓 ) )
28		df-clab	⊢ ( 𝑤 ∈ { 𝑦 ∣ 𝜓 } ↔ [ 𝑤 / 𝑦 ] 𝜓 )
29	27 28	syl6rbbr	⊢ ( 𝑤 = 𝑦 → ( 𝑤 ∈ { 𝑦 ∣ 𝜓 } ↔ 𝜓 ) )
30	25 29	anbi12d	⊢ ( 𝑤 = 𝑦 → ( ( 𝑧 = ⟨ 𝑥 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦 ∣ 𝜓 } ) ↔ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) )
31	22 23 30	cbvexv1	⊢ ( ∃ 𝑤 ( 𝑧 = ⟨ 𝑥 , 𝑤 ⟩ ∧ 𝑤 ∈ { 𝑦 ∣ 𝜓 } ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) )
32	6 19 31	3bitri	⊢ ( 𝑧 ∈ ( { 𝑥 } × { 𝑦 ∣ 𝜓 } ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) )
33	32	anbi2i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ ( { 𝑥 } × { 𝑦 ∣ 𝜓 } ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) )
34	3 5 33	3bitr4ri	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ ( { 𝑥 } × { 𝑦 ∣ 𝜓 } ) ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) )
35	34	exbii	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ ( { 𝑥 } × { 𝑦 ∣ 𝜓 } ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) )
36		eliun	⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { 𝑦 ∣ 𝜓 } ) ↔ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ ( { 𝑥 } × { 𝑦 ∣ 𝜓 } ) )
37		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ ( { 𝑥 } × { 𝑦 ∣ 𝜓 } ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ ( { 𝑥 } × { 𝑦 ∣ 𝜓 } ) ) )
38	36 37	bitri	⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { 𝑦 ∣ 𝜓 } ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ ( { 𝑥 } × { 𝑦 ∣ 𝜓 } ) ) )
39		elopab	⊢ ( 𝑧 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) )
40	35 38 39	3bitr4i	⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { 𝑦 ∣ 𝜓 } ) ↔ 𝑧 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } )
41	40	eqriv	⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { 𝑦 ∣ 𝜓 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) }
42		snex	⊢ { 𝑥 } ∈ V
43		xpexg	⊢ ( ( { 𝑥 } ∈ V ∧ { 𝑦 ∣ 𝜓 } ∈ V ) → ( { 𝑥 } × { 𝑦 ∣ 𝜓 } ) ∈ V )
44	42 2 43	sylancr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( { 𝑥 } × { 𝑦 ∣ 𝜓 } ) ∈ V )
45	44	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( { 𝑥 } × { 𝑦 ∣ 𝜓 } ) ∈ V )
46		iunexg	⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑥 ∈ 𝐴 ( { 𝑥 } × { 𝑦 ∣ 𝜓 } ) ∈ V ) → ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { 𝑦 ∣ 𝜓 } ) ∈ V )
47	1 45 46	syl2anc	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { 𝑦 ∣ 𝜓 } ) ∈ V )
48	41 47	eqeltrrid	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } ∈ V )