Metamath Proof Explorer

Theorem functhinclem3

Description: Lemma for functhinc . The mapped morphism is in its corresponding hom-set. (Contributed by Zhi Wang, 1-Oct-2024)

Ref Expression
Hypotheses functhinclem3.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
functhinclem3.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
functhinclem3.m ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 𝐻 𝑌 ) )
functhinclem3.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝐻 𝑦 ) × ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) ) )
functhinclem3.1 ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) = ∅ → ( 𝑋 𝐻 𝑌 ) = ∅ ) )
functhinclem3.2 ⊢ ( 𝜑 → ∃* 𝑛 𝑛 ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
Assertion functhinclem3 ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 functhinclem3.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
2 functhinclem3.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
3 functhinclem3.m ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 𝐻 𝑌 ) )
4 functhinclem3.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝐻 𝑦 ) × ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) ) )
5 functhinclem3.1 ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) = ∅ → ( 𝑋 𝐻 𝑌 ) = ∅ ) )
6 functhinclem3.2 ⊢ ( 𝜑 → ∃* 𝑛 𝑛 ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
7 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 𝑥 = 𝑋 )
8 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 𝑦 = 𝑌 )
9 7 8 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑌 ) )
10 7 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
11 8 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑌 ) )
12 10 11 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
13 9 12 xpeq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( ( 𝑥 𝐻 𝑦 ) × ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝑋 𝐻 𝑌 ) × ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) )
14 ovex ⊢ ( 𝑋 𝐻 𝑌 ) ∈ V
15 ovex ⊢ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ∈ V
16 14 15 xpex ⊢ ( ( 𝑋 𝐻 𝑌 ) × ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) ∈ V
17 16 a1i ⊢ ( 𝜑 → ( ( 𝑋 𝐻 𝑌 ) × ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) ∈ V )
18 4 13 1 2 17 ovmpod ⊢ ( 𝜑 → ( 𝑋 𝐺 𝑌 ) = ( ( 𝑋 𝐻 𝑌 ) × ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) )
19 eqid ⊢ ( ( 𝑋 𝐻 𝑌 ) × ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) = ( ( 𝑋 𝐻 𝑌 ) × ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
20 19 5 6 mofeu ⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ↔ ( 𝑋 𝐺 𝑌 ) = ( ( 𝑋 𝐻 𝑌 ) × ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) ) )
21 18 20 mpbird ⊢ ( 𝜑 → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
22 21 3 ffvelrnd ⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )