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

Metamath Proof Explorer

Theorem elovmporab

Description: Implications for the value of an operation, defined by the maps-to notation with a class abstraction as a result, having an element. (Contributed by Alexander van der Vekens, 15-Jul-2018)

Ref Expression
Hypotheses elovmporab.o ⊢ 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑧 ∈ 𝑀 ∣ 𝜑 } )
elovmporab.v ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → 𝑀 ∈ V )
Assertion elovmporab ( 𝑍 ∈ ( 𝑋 𝑂 𝑌 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 elovmporab.o ⊢ 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑧 ∈ 𝑀 ∣ 𝜑 } )
2 elovmporab.v ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → 𝑀 ∈ V )
3 1 elmpocl ⊢ ( 𝑍 ∈ ( 𝑋 𝑂 𝑌 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
4 1 a1i ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑧 ∈ 𝑀 ∣ 𝜑 } ) )
5 sbceq1a ⊢ ( 𝑦 = 𝑌 → ( 𝜑 ↔ [ 𝑌 / 𝑦 ] 𝜑 ) )
6 sbceq1a ⊢ ( 𝑥 = 𝑋 → ( [ 𝑌 / 𝑦 ] 𝜑 ↔ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) )
7 5 6 sylan9bbr ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝜑 ↔ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) )
8 7 adantl ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝜑 ↔ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) )
9 8 rabbidv ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → { 𝑧 ∈ 𝑀 ∣ 𝜑 } = { 𝑧 ∈ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } )
10 eqidd ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ 𝑥 = 𝑋 ) → V = V )
11 simpl ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → 𝑋 ∈ V )
12 simpr ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → 𝑌 ∈ V )
13 rabexg ⊢ ( 𝑀 ∈ V → { 𝑧 ∈ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ∈ V )
14 2 13 syl ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → { 𝑧 ∈ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ∈ V )
15 nfcv ⊢ Ⅎ 𝑥 𝑋
16 15 nfel1 ⊢ Ⅎ 𝑥 𝑋 ∈ V
17 nfcv ⊢ Ⅎ 𝑥 𝑌
18 17 nfel1 ⊢ Ⅎ 𝑥 𝑌 ∈ V
19 16 18 nfan ⊢ Ⅎ 𝑥 ( 𝑋 ∈ V ∧ 𝑌 ∈ V )
20 nfcv ⊢ Ⅎ 𝑦 𝑋
21 20 nfel1 ⊢ Ⅎ 𝑦 𝑋 ∈ V
22 nfcv ⊢ Ⅎ 𝑦 𝑌
23 22 nfel1 ⊢ Ⅎ 𝑦 𝑌 ∈ V
24 21 23 nfan ⊢ Ⅎ 𝑦 ( 𝑋 ∈ V ∧ 𝑌 ∈ V )
25 nfsbc1v ⊢ Ⅎ 𝑥 [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑
26 nfcv ⊢ Ⅎ 𝑥 𝑀
27 25 26 nfrabw ⊢ Ⅎ 𝑥 { 𝑧 ∈ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 }
28 nfsbc1v ⊢ Ⅎ 𝑦 [ 𝑌 / 𝑦 ] 𝜑
29 20 28 nfsbcw ⊢ Ⅎ 𝑦 [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑
30 nfcv ⊢ Ⅎ 𝑦 𝑀
31 29 30 nfrabw ⊢ Ⅎ 𝑦 { 𝑧 ∈ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 }
32 4 9 10 11 12 14 19 24 20 17 27 31 ovmpodxf ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑋 𝑂 𝑌 ) = { 𝑧 ∈ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } )
33 32 eleq2d ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑍 ∈ ( 𝑋 𝑂 𝑌 ) ↔ 𝑍 ∈ { 𝑧 ∈ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ) )
34 df-3an ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ 𝑀 ) ↔ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ 𝑍 ∈ 𝑀 ) )
35 34 simplbi2com ⊢ ( 𝑍 ∈ 𝑀 → ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ 𝑀 ) ) )
36 elrabi ⊢ ( 𝑍 ∈ { 𝑧 ∈ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } → 𝑍 ∈ 𝑀 )
37 35 36 syl11 ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑍 ∈ { 𝑧 ∈ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ 𝑀 ) ) )
38 33 37 sylbid ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑍 ∈ ( 𝑋 𝑂 𝑌 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ 𝑀 ) ) )
39 3 38 mpcom ⊢ ( 𝑍 ∈ ( 𝑋 𝑂 𝑌 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ 𝑀 ) )