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 ⊢ G ∈ ⨉ z ∈ B × B F ⁡ 1 st ⁡ z J F ⁡ 2 nd ⁡ z H ⁡ z ↔ G ∈ V ∧ G Fn B × B ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ F ⁡ x J F ⁡ y

Proof

Step Hyp Ref Expression
1 elixp2 ⊢ G ∈ ⨉ z ∈ B × B F ⁡ 1 st ⁡ z J F ⁡ 2 nd ⁡ z H ⁡ z ↔ G ∈ V ∧ G Fn B × B ∧ ∀ z ∈ B × B G ⁡ z ∈ F ⁡ 1 st ⁡ z J F ⁡ 2 nd ⁡ z H ⁡ z
2 fveq2 ⊢ z = x y → G ⁡ z = G ⁡ x y
3 df-ov ⊢ x G y = G ⁡ x y
4 2 3 eqtr4di ⊢ z = x y → G ⁡ z = x G y
5 vex ⊢ x ∈ V
6 vex ⊢ y ∈ V
7 5 6 op1std ⊢ z = x y → 1 st ⁡ z = x
8 7 fveq2d ⊢ z = x y → F ⁡ 1 st ⁡ z = F ⁡ x
9 5 6 op2ndd ⊢ z = x y → 2 nd ⁡ z = y
10 9 fveq2d ⊢ z = x y → F ⁡ 2 nd ⁡ z = F ⁡ y
11 8 10 oveq12d ⊢ z = x y → F ⁡ 1 st ⁡ z J F ⁡ 2 nd ⁡ z = F ⁡ x J F ⁡ y
12 fveq2 ⊢ z = x y → H ⁡ z = H ⁡ x y
13 df-ov ⊢ x H y = H ⁡ x y
14 12 13 eqtr4di ⊢ z = x y → H ⁡ z = x H y
15 11 14 oveq12d ⊢ z = x y → F ⁡ 1 st ⁡ z J F ⁡ 2 nd ⁡ z H ⁡ z = F ⁡ x J F ⁡ y x H y
16 4 15 eleq12d ⊢ z = x y → G ⁡ z ∈ F ⁡ 1 st ⁡ z J F ⁡ 2 nd ⁡ z H ⁡ z ↔ x G y ∈ F ⁡ x J F ⁡ y x H y
17 ovex ⊢ F ⁡ x J F ⁡ y ∈ V
18 ovex ⊢ x H y ∈ V
19 17 18 elmap ⊢ x G y ∈ F ⁡ x J F ⁡ y x H y ↔ x G y : x H y ⟶ F ⁡ x J F ⁡ y
20 16 19 bitrdi ⊢ z = x y → G ⁡ z ∈ F ⁡ 1 st ⁡ z J F ⁡ 2 nd ⁡ z H ⁡ z ↔ x G y : x H y ⟶ F ⁡ x J F ⁡ y
21 20 ralxp ⊢ ∀ z ∈ B × B G ⁡ z ∈ F ⁡ 1 st ⁡ z J F ⁡ 2 nd ⁡ z H ⁡ z ↔ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ F ⁡ x J F ⁡ y
22 21 3anbi3i ⊢ G ∈ V ∧ G Fn B × B ∧ ∀ z ∈ B × B G ⁡ z ∈ F ⁡ 1 st ⁡ z J F ⁡ 2 nd ⁡ z H ⁡ z ↔ G ∈ V ∧ G Fn B × B ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ F ⁡ x J F ⁡ y
23 1 22 bitri ⊢ G ∈ ⨉ z ∈ B × B F ⁡ 1 st ⁡ z J F ⁡ 2 nd ⁡ z H ⁡ z ↔ G ∈ V ∧ G Fn B × B ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ F ⁡ x J F ⁡ y