Theorem opabex3

Description: Existence of an ordered pair abstraction. (Contributed by Jeff Madsen, 2-Sep-2009)

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

Proof

Step	Hyp	Ref	Expression
1		opabex3.1	⊢ 𝐴 ∈ V
2		opabex3.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		df-clab	⊢ ( 𝑤 ∈ { 𝑦 ∣ 𝜑 } ↔ [ 𝑤 / 𝑦 ] 𝜑 )
27		sbequ12	⊢ ( 𝑦 = 𝑤 → ( 𝜑 ↔ [ 𝑤 / 𝑦 ] 𝜑 ) )
28	27	equcoms	⊢ ( 𝑤 = 𝑦 → ( 𝜑 ↔ [ 𝑤 / 𝑦 ] 𝜑 ) )
29	26 28	bitr4id	⊢ ( 𝑤 = 𝑦 → ( 𝑤 ∈ { 𝑦 ∣ 𝜑 } ↔ 𝜑 ) )
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	rgen	⊢ ∀ 𝑥 ∈ 𝐴 ( { 𝑥 } × { 𝑦 ∣ 𝜑 } ) ∈ V
46		iunexg	⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑥 ∈ 𝐴 ( { 𝑥 } × { 𝑦 ∣ 𝜑 } ) ∈ V ) → ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { 𝑦 ∣ 𝜑 } ) ∈ V )
47	1 45 46	mp2an	⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { 𝑦 ∣ 𝜑 } ) ∈ V
48	41 47	eqeltrri	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∈ V