Metamath Proof Explorer

Theorem funcf2lem2

Description: A utility theorem for proving equivalence of "is a functor". (Contributed by Zhi Wang, 25-Sep-2025)

Ref Expression
Hypothesis funcf2lem2.b ⊢ 𝐵 = ( 𝐸 ‘ 𝐶 )
Assertion funcf2lem2 ( 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ↔ ( 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 funcf2lem2.b ⊢ 𝐵 = ( 𝐸 ‘ 𝐶 )
2 funcf2lem ⊢ ( 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ↔ ( 𝐺 ∈ V ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
3 3simpc ⊢ ( ( 𝐺 ∈ V ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
4 2 3 sylbi ⊢ ( 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) → ( 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
5 fnov ⊢ ( 𝐺 Fn ( 𝐵 × 𝐵 ) ↔ 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐺 𝑦 ) ) )
6 5 biimpi ⊢ ( 𝐺 Fn ( 𝐵 × 𝐵 ) → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐺 𝑦 ) ) )
7 1 fvexi ⊢ 𝐵 ∈ V
8 7 7 mpoex ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐺 𝑦 ) ) ∈ V
9 6 8 eqeltrdi ⊢ ( 𝐺 Fn ( 𝐵 × 𝐵 ) → 𝐺 ∈ V )
10 9 adantr ⊢ ( ( 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) → 𝐺 ∈ V )
11 simpl ⊢ ( ( 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) → 𝐺 Fn ( 𝐵 × 𝐵 ) )
12 simpr ⊢ ( ( 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
13 10 11 12 2 syl3anbrc ⊢ ( ( 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) → 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) )
14 4 13 impbii ⊢ ( 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ↔ ( 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )