Metamath Proof Explorer

Theorem funcf2lem

Description: A utility theorem for proving equivalence of "is a functor". (Contributed by Zhi Wang, 1-Oct-2024)

Ref Expression
Assertion funcf2lem ( 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ↔ ( 𝐺 ∈ V ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 elixp2 ⊢ ( 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ↔ ( 𝐺 ∈ V ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑧 ∈ ( 𝐵 × 𝐵 ) ( 𝐺 ‘ 𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) )
2 fveq2 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
3 df-ov ⊢ ( 𝑥 𝐺 𝑦 ) = ( 𝐺 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
4 2 3 eqtr4di ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐺 ‘ 𝑧 ) = ( 𝑥 𝐺 𝑦 ) )
5 vex ⊢ 𝑥 ∈ V
6 vex ⊢ 𝑦 ∈ V
7 5 6 op1std ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1st ‘ 𝑧 ) = 𝑥 )
8 7 fveq2d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) = ( 𝐹 ‘ 𝑥 ) )
9 5 6 op2ndd ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd ‘ 𝑧 ) = 𝑦 )
10 9 fveq2d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) = ( 𝐹 ‘ 𝑦 ) )
11 8 10 oveq12d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
12 fveq2 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐻 ‘ 𝑧 ) = ( 𝐻 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
13 df-ov ⊢ ( 𝑥 𝐻 𝑦 ) = ( 𝐻 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
14 12 13 eqtr4di ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐻 ‘ 𝑧 ) = ( 𝑥 𝐻 𝑦 ) )
15 11 14 oveq12d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ↑m ( 𝑥 𝐻 𝑦 ) ) )
16 4 15 eleq12d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐺 ‘ 𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ↔ ( 𝑥 𝐺 𝑦 ) ∈ ( ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ↑m ( 𝑥 𝐻 𝑦 ) ) ) )
17 ovex ⊢ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∈ V
18 ovex ⊢ ( 𝑥 𝐻 𝑦 ) ∈ V
19 17 18 elmap ⊢ ( ( 𝑥 𝐺 𝑦 ) ∈ ( ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ↑m ( 𝑥 𝐻 𝑦 ) ) ↔ ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
20 16 19 bitrdi ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐺 ‘ 𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ↔ ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
21 20 ralxp ⊢ ( ∀ 𝑧 ∈ ( 𝐵 × 𝐵 ) ( 𝐺 ‘ 𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
22 21 3anbi3i ⊢ ( ( 𝐺 ∈ V ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑧 ∈ ( 𝐵 × 𝐵 ) ( 𝐺 ‘ 𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ↔ ( 𝐺 ∈ V ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
23 1 22 bitri ⊢ ( 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ↔ ( 𝐺 ∈ V ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )