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

Metamath Proof Explorer

Theorem mptmpoopabbrdOLD

Description: Obsolete version of mptmpoopabbrd as of 7-Apr-2025. (Contributed by Alexander van Vekens, 8-Nov-2017) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 mptmpoopabbrd.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
2 mptmpoopabbrd.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 ‘ 𝐺 ) )
3 mptmpoopabbrd.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ‘ 𝐺 ) )
4 mptmpoopabbrd.1 ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → ( 𝜏 ↔ 𝜃 ) )
5 mptmpoopabbrd.2 ⊢ ( 𝑔 = 𝐺 → ( 𝜒 ↔ 𝜏 ) )
6 mptmpoopabbrd.m ⊢ 𝑀 = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( 𝐴 ‘ 𝑔 ) , 𝑏 ∈ ( 𝐵 ‘ 𝑔 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜒 ∧ 𝑓 ( 𝐷 ‘ 𝑔 ) ℎ ) } ) )
7 fveq2 ⊢ ( 𝑔 = 𝐺 → ( 𝐴 ‘ 𝑔 ) = ( 𝐴 ‘ 𝐺 ) )
8 fveq2 ⊢ ( 𝑔 = 𝐺 → ( 𝐵 ‘ 𝑔 ) = ( 𝐵 ‘ 𝐺 ) )
9 fveq2 ⊢ ( 𝑔 = 𝐺 → ( 𝐷 ‘ 𝑔 ) = ( 𝐷 ‘ 𝐺 ) )
10 9 breqd ⊢ ( 𝑔 = 𝐺 → ( 𝑓 ( 𝐷 ‘ 𝑔 ) ℎ ↔ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) )
11 5 10 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝜒 ∧ 𝑓 ( 𝐷 ‘ 𝑔 ) ℎ ) ↔ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) ) )
12 11 opabbidv ⊢ ( 𝑔 = 𝐺 → { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜒 ∧ 𝑓 ( 𝐷 ‘ 𝑔 ) ℎ ) } = { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } )
13 7 8 12 mpoeq123dv ⊢ ( 𝑔 = 𝐺 → ( 𝑎 ∈ ( 𝐴 ‘ 𝑔 ) , 𝑏 ∈ ( 𝐵 ‘ 𝑔 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜒 ∧ 𝑓 ( 𝐷 ‘ 𝑔 ) ℎ ) } ) = ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) )
14 1 elexd ⊢ ( 𝜑 → 𝐺 ∈ V )
15 fvex ⊢ ( 𝐴 ‘ 𝐺 ) ∈ V
16 fvex ⊢ ( 𝐵 ‘ 𝐺 ) ∈ V
17 15 16 mpoex ⊢ ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) ∈ V
18 17 a1i ⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) ∈ V )
19 6 13 14 18 fvmptd3 ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐺 ) = ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) )
20 19 oveqd ⊢ ( 𝜑 → ( 𝑋 ( 𝑀 ‘ 𝐺 ) 𝑌 ) = ( 𝑋 ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) 𝑌 ) )
21 4 anbi1d ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → ( ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) ↔ ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) ) )
22 21 opabbidv ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } = { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } )
23 eqid ⊢ ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) = ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } )
24 ancom ⊢ ( ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) ↔ ( 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ∧ 𝜃 ) )
25 24 opabbii ⊢ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } = { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ∧ 𝜃 ) }
26 opabresex2 ⊢ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ∧ 𝜃 ) } ∈ V
27 25 26 eqeltri ⊢ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ∈ V
28 22 23 27 ovmpoa ⊢ ( ( 𝑋 ∈ ( 𝐴 ‘ 𝐺 ) ∧ 𝑌 ∈ ( 𝐵 ‘ 𝐺 ) ) → ( 𝑋 ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) 𝑌 ) = { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } )
29 2 3 28 syl2anc ⊢ ( 𝜑 → ( 𝑋 ( 𝑎 ∈ ( 𝐴 ‘ 𝐺 ) , 𝑏 ∈ ( 𝐵 ‘ 𝐺 ) ↦ { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜏 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } ) 𝑌 ) = { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } )
30 20 29 eqtrd ⊢ ( 𝜑 → ( 𝑋 ( 𝑀 ‘ 𝐺 ) 𝑌 ) = { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝜃 ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } )