Metamath Proof Explorer

Theorem mptmpoopabbrdOLDOLD

Description: Obsolete version of mptmpoopabbrd as of 13-Dec-2024. (Contributed by Alexander van Vekens, 8-Nov-2017) (Revised by AV, 15-Jan-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses mptmpoopabbrdOLD.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
mptmpoopabbrdOLD.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 ‘ 𝐺 ) )
mptmpoopabbrdOLD.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ‘ 𝐺 ) )
mptmpoopabbrdOLD.v ⊢ ( 𝜑 → { ⟨ 𝑓 , ℎ ⟩ ∣ 𝜓 } ∈ 𝑉 )
mptmpoopabbrdOLD.r ⊢ ( ( 𝜑 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) → 𝜓 )
mptmpoopabbrdOLD.1 ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → ( 𝜏 ↔ 𝜃 ) )
mptmpoopabbrdOLD.2 ⊢ ( 𝑔 = 𝐺 → ( 𝜒 ↔ 𝜏 ) )
mptmpoopabbrdOLD.m ⊢ 𝑀 = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( 𝐴 ‘ 𝑔 ) , 𝑏 ∈ ( 𝐵 ‘ 𝑔 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜒 ∧ 𝑓 ( 𝐷 ‘ 𝑔 ) ℎ ) } ) )
Assertion mptmpoopabbrdOLDOLD ( 𝜑 → ( 𝑋 ( 𝑀 ‘ 𝐺 ) 𝑌 ) = { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } )

Proof

Step Hyp Ref Expression
1 mptmpoopabbrdOLD.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
2 mptmpoopabbrdOLD.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 ‘ 𝐺 ) )
3 mptmpoopabbrdOLD.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ‘ 𝐺 ) )
4 mptmpoopabbrdOLD.v ⊢ ( 𝜑 → { ⟨ 𝑓 , ℎ ⟩ ∣ 𝜓 } ∈ 𝑉 )
5 mptmpoopabbrdOLD.r ⊢ ( ( 𝜑 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) → 𝜓 )
6 mptmpoopabbrdOLD.1 ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → ( 𝜏 ↔ 𝜃 ) )
7 mptmpoopabbrdOLD.2 ⊢ ( 𝑔 = 𝐺 → ( 𝜒 ↔ 𝜏 ) )
8 mptmpoopabbrdOLD.m ⊢ 𝑀 = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( 𝐴 ‘ 𝑔 ) , 𝑏 ∈ ( 𝐵 ‘ 𝑔 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜒 ∧ 𝑓 ( 𝐷 ‘ 𝑔 ) ℎ ) } ) )
9 fveq2 ⊢ ( 𝑔 = 𝐺 → ( 𝐴 ‘ 𝑔 ) = ( 𝐴 ‘ 𝐺 ) )
10 fveq2 ⊢ ( 𝑔 = 𝐺 → ( 𝐵 ‘ 𝑔 ) = ( 𝐵 ‘ 𝐺 ) )
11 fveq2 ⊢ ( 𝑔 = 𝐺 → ( 𝐷 ‘ 𝑔 ) = ( 𝐷 ‘ 𝐺 ) )
12 11 breqd ⊢ ( 𝑔 = 𝐺 → ( 𝑓 ( 𝐷 ‘ 𝑔 ) ℎ ↔ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) )
13 7 12 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝜒 ∧ 𝑓 ( 𝐷 ‘ 𝑔 ) ℎ ) ↔ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) ) )
14 13 opabbidv ⊢ ( 𝑔 = 𝐺 → { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜒 ∧ 𝑓 ( 𝐷 ‘ 𝑔 ) ℎ ) } = { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } )
15 9 10 14 mpoeq123dv ⊢ ( 𝑔 = 𝐺 → ( 𝑎 ∈ ( 𝐴 ‘ 𝑔 ) , 𝑏 ∈ ( 𝐵 ‘ 𝑔 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜒 ∧ 𝑓 ( 𝐷 ‘ 𝑔 ) ℎ ) } ) = ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) )
16 elex ⊢ ( 𝐺 ∈ 𝑊 → 𝐺 ∈ V )
17 16 adantr ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐺 ∈ 𝑊 ) → 𝐺 ∈ V )
18 fvex ⊢ ( 𝐴 ‘ 𝐺 ) ∈ V
19 fvex ⊢ ( 𝐵 ‘ 𝐺 ) ∈ V
20 18 19 pm3.2i ⊢ ( ( 𝐴 ‘ 𝐺 ) ∈ V ∧ ( 𝐵 ‘ 𝐺 ) ∈ V )
21 mpoexga ⊢ ( ( ( 𝐴 ‘ 𝐺 ) ∈ V ∧ ( 𝐵 ‘ 𝐺 ) ∈ V ) → ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) ∈ V )
22 20 21 mp1i ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐺 ∈ 𝑊 ) → ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) ∈ V )
23 8 15 17 22 fvmptd3 ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐺 ∈ 𝑊 ) → ( 𝑀 ‘ 𝐺 ) = ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) )
24 1 1 23 syl2anc ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐺 ) = ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) )
25 24 oveqd ⊢ ( 𝜑 → ( 𝑋 ( 𝑀 ‘ 𝐺 ) 𝑌 ) = ( 𝑋 ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) 𝑌 ) )
26 ancom ⊢ ( ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) ↔ ( 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ∧ 𝜃 ) )
27 26 opabbii ⊢ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } = { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ∧ 𝜃 ) }
28 5 4 opabresex2d ⊢ ( 𝜑 → { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ∧ 𝜃 ) } ∈ V )
29 27 28 eqeltrid ⊢ ( 𝜑 → { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ∈ V )
30 6 anbi1d ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → ( ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) ↔ ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) ) )
31 30 opabbidv ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } = { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } )
32 eqid ⊢ ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) = ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } )
33 31 32 ovmpoga ⊢ ( ( 𝑋 ∈ ( 𝐴 ‘ 𝐺 ) ∧ 𝑌 ∈ ( 𝐵 ‘ 𝐺 ) ∧ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ∈ V ) → ( 𝑋 ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) 𝑌 ) = { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } )
34 2 3 29 33 syl3anc ⊢ ( 𝜑 → ( 𝑋 ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) 𝑌 ) = { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } )
35 25 34 eqtrd ⊢ ( 𝜑 → ( 𝑋 ( 𝑀 ‘ 𝐺 ) 𝑌 ) = { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } )