Theorem opabex3rd

Description: Existence of an ordered pair abstraction if the second components are elements of a set. (Contributed by AV, 17-Sep-2023) (Revised by AV, 9-Aug-2024)

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

Proof

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