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 ⊢ B = E ⁡ C
Assertion funcf2lem2 ⊢ G ∈ ⨉ z ∈ B × B F ⁡ 1 st ⁡ z J F ⁡ 2 nd ⁡ z H ⁡ z ↔ 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 funcf2lem2.b ⊢ B = E ⁡ C
2 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
3 3simpc ⊢ G ∈ V ∧ G Fn B × B ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ F ⁡ x J F ⁡ y → G Fn B × B ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ F ⁡ x J F ⁡ y
4 2 3 sylbi ⊢ G ∈ ⨉ z ∈ B × B F ⁡ 1 st ⁡ z J F ⁡ 2 nd ⁡ z H ⁡ z → G Fn B × B ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ F ⁡ x J F ⁡ y
5 fnov ⊢ G Fn B × B ↔ G = x ∈ B , y ∈ B ⟼ x G y
6 5 biimpi ⊢ G Fn B × B → G = x ∈ B , y ∈ B ⟼ x G y
7 1 fvexi ⊢ B ∈ V
8 7 7 mpoex ⊢ x ∈ B , y ∈ B ⟼ x G y ∈ V
9 6 8 eqeltrdi ⊢ G Fn B × B → G ∈ V
10 9 adantr ⊢ G Fn B × B ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ F ⁡ x J F ⁡ y → G ∈ V
11 simpl ⊢ G Fn B × B ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ F ⁡ x J F ⁡ y → G Fn B × B
12 simpr ⊢ G Fn B × B ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ F ⁡ x J F ⁡ y → ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ F ⁡ x J F ⁡ y
13 10 11 12 2 syl3anbrc ⊢ G Fn B × B ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ F ⁡ x J F ⁡ y → G ∈ ⨉ z ∈ B × B F ⁡ 1 st ⁡ z J F ⁡ 2 nd ⁡ z H ⁡ z
14 4 13 impbii ⊢ G ∈ ⨉ z ∈ B × B F ⁡ 1 st ⁡ z J F ⁡ 2 nd ⁡ z H ⁡ z ↔ G Fn B × B ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ F ⁡ x J F ⁡ y