Metamath Proof Explorer


Theorem elovmporab1

Description: Implications for the value of an operation, defined by the maps-to notation with a class abstraction as a result, having an element. Here, the base set of the class abstraction depends on the first operand. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker elovmporab1w when possible. (Contributed by Alexander van der Vekens, 15-Jul-2018) (New usage is discouraged.)

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

Proof

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