This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 vsnex ⊢ { 𝑦 } ∈ 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 )