Metamath Proof Explorer

Theorem elovmpt3rab1

Description: Implications for the value of an operation defined by the maps-to notation with a function into a class abstraction as a result having an element. The domain of the function and the base set of the class abstraction may depend on the operands, using implicit substitution. (Contributed by AV, 16-Jul-2018) (Revised by AV, 16-May-2019)

Ref Expression
Hypotheses ovmpt3rab1.o ⊢ 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑧 ∈ 𝑀 ↦ { 𝑎 ∈ 𝑁 ∣ 𝜑 } ) )
ovmpt3rab1.m ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑀 = 𝐾 )
ovmpt3rab1.n ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑁 = 𝐿 )
Assertion elovmpt3rab1 ( ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) → ( 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) → ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝑍 ∈ 𝐾 ∧ 𝐴 ∈ 𝐿 ) ) ) )

Proof

Step Hyp Ref Expression
1 ovmpt3rab1.o ⊢ 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑧 ∈ 𝑀 ↦ { 𝑎 ∈ 𝑁 ∣ 𝜑 } ) )
2 ovmpt3rab1.m ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑀 = 𝐾 )
3 ovmpt3rab1.n ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑁 = 𝐿 )
4 1 elovmpt3imp ⊢ ( 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
5 simprl ⊢ ( ( 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) ∧ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
6 elfvdm ⊢ ( 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) → 𝑍 ∈ dom ( 𝑋 𝑂 𝑌 ) )
7 simpl ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → 𝑋 ∈ V )
8 7 adantr ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) → 𝑋 ∈ V )
9 simplr ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) → 𝑌 ∈ V )
10 simprl ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) → 𝐾 ∈ 𝑈 )
11 simprr ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) → 𝐿 ∈ 𝑇 )
12 1 2 3 ovmpt3rabdm ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝐾 ∈ 𝑈 ) ∧ 𝐿 ∈ 𝑇 ) → dom ( 𝑋 𝑂 𝑌 ) = 𝐾 )
13 8 9 10 11 12 syl31anc ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) → dom ( 𝑋 𝑂 𝑌 ) = 𝐾 )
14 13 eleq2d ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) → ( 𝑍 ∈ dom ( 𝑋 𝑂 𝑌 ) ↔ 𝑍 ∈ 𝐾 ) )
15 14 biimpcd ⊢ ( 𝑍 ∈ dom ( 𝑋 𝑂 𝑌 ) → ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) → 𝑍 ∈ 𝐾 ) )
16 15 adantr ⊢ ( ( 𝑍 ∈ dom ( 𝑋 𝑂 𝑌 ) ∧ 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) ) → ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) → 𝑍 ∈ 𝐾 ) )
17 16 imp ⊢ ( ( ( 𝑍 ∈ dom ( 𝑋 𝑂 𝑌 ) ∧ 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) ) ∧ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) ) → 𝑍 ∈ 𝐾 )
18 simpl ⊢ ( ( 𝑍 ∈ 𝐾 ∧ ( ( 𝑍 ∈ dom ( 𝑋 𝑂 𝑌 ) ∧ 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) ) ∧ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) ) ) → 𝑍 ∈ 𝐾 )
19 simplr ⊢ ( ( ( 𝑍 ∈ dom ( 𝑋 𝑂 𝑌 ) ∧ 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) ) ∧ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) ) → 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) )
20 19 adantl ⊢ ( ( 𝑍 ∈ 𝐾 ∧ ( ( 𝑍 ∈ dom ( 𝑋 𝑂 𝑌 ) ∧ 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) ) ∧ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) ) ) → 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) )
21 simpl ⊢ ( ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) → 𝐾 ∈ 𝑈 )
22 21 anim2i ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) → ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ 𝐾 ∈ 𝑈 ) )
23 df-3an ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝐾 ∈ 𝑈 ) ↔ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ 𝐾 ∈ 𝑈 ) )
24 22 23 sylibr ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝐾 ∈ 𝑈 ) )
25 24 ad2antll ⊢ ( ( 𝑍 ∈ 𝐾 ∧ ( ( 𝑍 ∈ dom ( 𝑋 𝑂 𝑌 ) ∧ 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) ) ∧ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) ) ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝐾 ∈ 𝑈 ) )
26 sbceq1a ⊢ ( 𝑦 = 𝑌 → ( 𝜑 ↔ [ 𝑌 / 𝑦 ] 𝜑 ) )
27 sbceq1a ⊢ ( 𝑥 = 𝑋 → ( [ 𝑌 / 𝑦 ] 𝜑 ↔ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) )
28 26 27 sylan9bbr ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝜑 ↔ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) )
29 nfsbc1v ⊢ Ⅎ 𝑥 [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑
30 nfcv ⊢ Ⅎ 𝑦 𝑋
31 nfsbc1v ⊢ Ⅎ 𝑦 [ 𝑌 / 𝑦 ] 𝜑
32 30 31 nfsbcw ⊢ Ⅎ 𝑦 [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑
33 1 2 3 28 29 32 ovmpt3rab1 ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝐾 ∈ 𝑈 ) → ( 𝑋 𝑂 𝑌 ) = ( 𝑧 ∈ 𝐾 ↦ { 𝑎 ∈ 𝐿 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ) )
34 33 fveq1d ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝐾 ∈ 𝑈 ) → ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) = ( ( 𝑧 ∈ 𝐾 ↦ { 𝑎 ∈ 𝐿 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ) ‘ 𝑍 ) )
35 25 34 syl ⊢ ( ( 𝑍 ∈ 𝐾 ∧ ( ( 𝑍 ∈ dom ( 𝑋 𝑂 𝑌 ) ∧ 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) ) ∧ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) ) ) → ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) = ( ( 𝑧 ∈ 𝐾 ↦ { 𝑎 ∈ 𝐿 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ) ‘ 𝑍 ) )
36 rabexg ⊢ ( 𝐿 ∈ 𝑇 → { 𝑎 ∈ 𝐿 ∣ [ 𝑍 / 𝑧 ] [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ∈ V )
37 36 adantl ⊢ ( ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) → { 𝑎 ∈ 𝐿 ∣ [ 𝑍 / 𝑧 ] [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ∈ V )
38 37 ad2antll ⊢ ( ( ( 𝑍 ∈ dom ( 𝑋 𝑂 𝑌 ) ∧ 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) ) ∧ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) ) → { 𝑎 ∈ 𝐿 ∣ [ 𝑍 / 𝑧 ] [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ∈ V )
39 nfcv ⊢ Ⅎ 𝑧 𝑍
40 nfsbc1v ⊢ Ⅎ 𝑧 [ 𝑍 / 𝑧 ] [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑
41 nfcv ⊢ Ⅎ 𝑧 𝐿
42 40 41 nfrabw ⊢ Ⅎ 𝑧 { 𝑎 ∈ 𝐿 ∣ [ 𝑍 / 𝑧 ] [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 }
43 sbceq1a ⊢ ( 𝑧 = 𝑍 → ( [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ↔ [ 𝑍 / 𝑧 ] [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) )
44 43 rabbidv ⊢ ( 𝑧 = 𝑍 → { 𝑎 ∈ 𝐿 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } = { 𝑎 ∈ 𝐿 ∣ [ 𝑍 / 𝑧 ] [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } )
45 eqid ⊢ ( 𝑧 ∈ 𝐾 ↦ { 𝑎 ∈ 𝐿 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ) = ( 𝑧 ∈ 𝐾 ↦ { 𝑎 ∈ 𝐿 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } )
46 39 42 44 45 fvmptf ⊢ ( ( 𝑍 ∈ 𝐾 ∧ { 𝑎 ∈ 𝐿 ∣ [ 𝑍 / 𝑧 ] [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ∈ V ) → ( ( 𝑧 ∈ 𝐾 ↦ { 𝑎 ∈ 𝐿 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ) ‘ 𝑍 ) = { 𝑎 ∈ 𝐿 ∣ [ 𝑍 / 𝑧 ] [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } )
47 38 46 sylan2 ⊢ ( ( 𝑍 ∈ 𝐾 ∧ ( ( 𝑍 ∈ dom ( 𝑋 𝑂 𝑌 ) ∧ 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) ) ∧ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) ) ) → ( ( 𝑧 ∈ 𝐾 ↦ { 𝑎 ∈ 𝐿 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ) ‘ 𝑍 ) = { 𝑎 ∈ 𝐿 ∣ [ 𝑍 / 𝑧 ] [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } )
48 35 47 eqtr2d ⊢ ( ( 𝑍 ∈ 𝐾 ∧ ( ( 𝑍 ∈ dom ( 𝑋 𝑂 𝑌 ) ∧ 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) ) ∧ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) ) ) → { 𝑎 ∈ 𝐿 ∣ [ 𝑍 / 𝑧 ] [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } = ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) )
49 20 48 eleqtrrd ⊢ ( ( 𝑍 ∈ 𝐾 ∧ ( ( 𝑍 ∈ dom ( 𝑋 𝑂 𝑌 ) ∧ 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) ) ∧ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) ) ) → 𝐴 ∈ { 𝑎 ∈ 𝐿 ∣ [ 𝑍 / 𝑧 ] [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } )
50 elrabi ⊢ ( 𝐴 ∈ { 𝑎 ∈ 𝐿 ∣ [ 𝑍 / 𝑧 ] [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } → 𝐴 ∈ 𝐿 )
51 49 50 syl ⊢ ( ( 𝑍 ∈ 𝐾 ∧ ( ( 𝑍 ∈ dom ( 𝑋 𝑂 𝑌 ) ∧ 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) ) ∧ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) ) ) → 𝐴 ∈ 𝐿 )
52 18 51 jca ⊢ ( ( 𝑍 ∈ 𝐾 ∧ ( ( 𝑍 ∈ dom ( 𝑋 𝑂 𝑌 ) ∧ 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) ) ∧ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) ) ) → ( 𝑍 ∈ 𝐾 ∧ 𝐴 ∈ 𝐿 ) )
53 17 52 mpancom ⊢ ( ( ( 𝑍 ∈ dom ( 𝑋 𝑂 𝑌 ) ∧ 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) ) ∧ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) ) → ( 𝑍 ∈ 𝐾 ∧ 𝐴 ∈ 𝐿 ) )
54 53 exp31 ⊢ ( 𝑍 ∈ dom ( 𝑋 𝑂 𝑌 ) → ( 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) → ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) → ( 𝑍 ∈ 𝐾 ∧ 𝐴 ∈ 𝐿 ) ) ) )
55 6 54 mpcom ⊢ ( 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) → ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) → ( 𝑍 ∈ 𝐾 ∧ 𝐴 ∈ 𝐿 ) ) )
56 55 imp ⊢ ( ( 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) ∧ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) ) → ( 𝑍 ∈ 𝐾 ∧ 𝐴 ∈ 𝐿 ) )
57 5 56 jca ⊢ ( ( 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) ∧ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) ) ) → ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝑍 ∈ 𝐾 ∧ 𝐴 ∈ 𝐿 ) ) )
58 57 exp32 ⊢ ( 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) → ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) → ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝑍 ∈ 𝐾 ∧ 𝐴 ∈ 𝐿 ) ) ) ) )
59 4 58 mpd ⊢ ( 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) → ( ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) → ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝑍 ∈ 𝐾 ∧ 𝐴 ∈ 𝐿 ) ) ) )
60 59 com12 ⊢ ( ( 𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇 ) → ( 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) → ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝑍 ∈ 𝐾 ∧ 𝐴 ∈ 𝐿 ) ) ) )