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

Metamath Proof Explorer

Theorem oprabv

Description: If a pair and a class are in a relationship given by a class abstraction of a collection of nested ordered pairs, the involved classes are sets. (Contributed by Alexander van der Vekens, 8-Jul-2018)

Ref Expression
Assertion oprabv ( ⟨ 𝑋 , 𝑌 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑍 → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V ) )

Proof

Step Hyp Ref Expression
1 reloprab ⊢ Rel { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
2 1 brrelex12i ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑍 → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ V ∧ 𝑍 ∈ V ) )
3 df-br ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑍 ↔ ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } )
4 opex ⊢ ⟨ 𝑋 , 𝑌 ⟩ ∈ V
5 nfcv ⊢ Ⅎ 𝑤 ⟨ 𝑋 , 𝑌 ⟩
6 5 nfeq1 ⊢ Ⅎ 𝑤 ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩
7 nfv ⊢ Ⅎ 𝑤 𝜑
8 6 7 nfan ⊢ Ⅎ 𝑤 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
9 8 nfex ⊢ Ⅎ 𝑤 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
10 9 nfex ⊢ Ⅎ 𝑤 ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
11 nfcv ⊢ Ⅎ 𝑧 ⟨ 𝑋 , 𝑌 ⟩
12 11 nfeq1 ⊢ Ⅎ 𝑧 ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩
13 nfsbc1v ⊢ Ⅎ 𝑧 [ 𝑍 / 𝑧 ] 𝜑
14 12 13 nfan ⊢ Ⅎ 𝑧 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑍 / 𝑧 ] 𝜑 )
15 14 nfex ⊢ Ⅎ 𝑧 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑍 / 𝑧 ] 𝜑 )
16 15 nfex ⊢ Ⅎ 𝑧 ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑍 / 𝑧 ] 𝜑 )
17 eqeq1 ⊢ ( 𝑤 = ⟨ 𝑋 , 𝑌 ⟩ → ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
18 17 anbi1d ⊢ ( 𝑤 = ⟨ 𝑋 , 𝑌 ⟩ → ( ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )
19 18 2exbidv ⊢ ( 𝑤 = ⟨ 𝑋 , 𝑌 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )
20 sbceq1a ⊢ ( 𝑧 = 𝑍 → ( 𝜑 ↔ [ 𝑍 / 𝑧 ] 𝜑 ) )
21 20 anbi2d ⊢ ( 𝑧 = 𝑍 → ( ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑍 / 𝑧 ] 𝜑 ) ) )
22 21 2exbidv ⊢ ( 𝑧 = 𝑍 → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑍 / 𝑧 ] 𝜑 ) ) )
23 10 16 19 22 opelopabgf ⊢ ( ( ⟨ 𝑋 , 𝑌 ⟩ ∈ V ∧ 𝑍 ∈ V ) → ( ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑍 / 𝑧 ] 𝜑 ) ) )
24 4 23 mpan ⊢ ( 𝑍 ∈ V → ( ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑍 / 𝑧 ] 𝜑 ) ) )
25 eqcom ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑋 , 𝑌 ⟩ )
26 vex ⊢ 𝑥 ∈ V
27 vex ⊢ 𝑦 ∈ V
28 26 27 opth ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑋 , 𝑌 ⟩ ↔ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) )
29 25 28 bitri ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) )
30 eqvisset ⊢ ( 𝑥 = 𝑋 → 𝑋 ∈ V )
31 eqvisset ⊢ ( 𝑦 = 𝑌 → 𝑌 ∈ V )
32 30 31 anim12i ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
33 29 32 sylbi ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
34 33 adantr ⊢ ( ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑍 / 𝑧 ] 𝜑 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
35 34 exlimivv ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑍 / 𝑧 ] 𝜑 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
36 35 anim1i ⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑍 / 𝑧 ] 𝜑 ) ∧ 𝑍 ∈ V ) → ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ 𝑍 ∈ V ) )
37 df-3an ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V ) ↔ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ 𝑍 ∈ V ) )
38 36 37 sylibr ⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑍 / 𝑧 ] 𝜑 ) ∧ 𝑍 ∈ V ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V ) )
39 38 expcom ⊢ ( 𝑍 ∈ V → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑍 / 𝑧 ] 𝜑 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V ) ) )
40 24 39 sylbid ⊢ ( 𝑍 ∈ V → ( ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V ) ) )
41 40 com12 ⊢ ( ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } → ( 𝑍 ∈ V → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V ) ) )
42 dfoprab2 ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }
43 41 42 eleq2s ⊢ ( ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } → ( 𝑍 ∈ V → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V ) ) )
44 3 43 sylbi ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑍 → ( 𝑍 ∈ V → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V ) ) )
45 44 com12 ⊢ ( 𝑍 ∈ V → ( ⟨ 𝑋 , 𝑌 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑍 → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V ) ) )
46 45 adantl ⊢ ( ( ⟨ 𝑋 , 𝑌 ⟩ ∈ V ∧ 𝑍 ∈ V ) → ( ⟨ 𝑋 , 𝑌 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑍 → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V ) ) )
47 2 46 mpcom ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑍 → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V ) )