Metamath Proof Explorer

Theorem isepi2

Description: Write out the epimorphism property directly. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses isepi.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
isepi.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
isepi.o ⊢ · = ( comp ‘ 𝐶 )
isepi.e ⊢ 𝐸 = ( Epi ‘ 𝐶 )
isepi.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
isepi.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
isepi.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion isepi2 ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ∀ ℎ ∈ ( 𝑌 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) = ( ℎ ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) → 𝑔 = ℎ ) ) ) )

Proof

Step Hyp Ref Expression
1 isepi.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 isepi.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 isepi.o ⊢ · = ( comp ‘ 𝐶 )
4 isepi.e ⊢ 𝐸 = ( Epi ‘ 𝐶 )
5 isepi.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
6 isepi.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7 isepi.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8 1 2 3 4 5 6 7 isepi ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∀ 𝑧 ∈ 𝐵 Fun ◡ ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ) ) ) )
9 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ) ) → 𝐶 ∈ Cat )
10 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ) ) → 𝑋 ∈ 𝐵 )
11 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ) ) → 𝑌 ∈ 𝐵 )
12 simprl ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ) ) → 𝑧 ∈ 𝐵 )
13 simplr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ) ) → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
14 simprr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ) ) → 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) )
15 1 2 3 9 10 11 12 13 14 catcocl ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑧 ) )
16 15 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ) → ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑧 ) )
17 16 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) ∧ 𝑧 ∈ 𝐵 ) → ∀ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑧 ) )
18 eqid ⊢ ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ) = ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) )
19 18 fmpt ⊢ ( ∀ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑧 ) ↔ ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ) : ( 𝑌 𝐻 𝑧 ) ⟶ ( 𝑋 𝐻 𝑧 ) )
20 df-f1 ⊢ ( ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ) : ( 𝑌 𝐻 𝑧 ) –1-1→ ( 𝑋 𝐻 𝑧 ) ↔ ( ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ) : ( 𝑌 𝐻 𝑧 ) ⟶ ( 𝑋 𝐻 𝑧 ) ∧ Fun ◡ ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ) ) )
21 20 baib ⊢ ( ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ) : ( 𝑌 𝐻 𝑧 ) ⟶ ( 𝑋 𝐻 𝑧 ) → ( ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ) : ( 𝑌 𝐻 𝑧 ) –1-1→ ( 𝑋 𝐻 𝑧 ) ↔ Fun ◡ ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ) ) )
22 19 21 sylbi ⊢ ( ∀ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑧 ) → ( ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ) : ( 𝑌 𝐻 𝑧 ) –1-1→ ( 𝑋 𝐻 𝑧 ) ↔ Fun ◡ ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ) ) )
23 oveq1 ⊢ ( 𝑔 = ℎ → ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) = ( ℎ ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) )
24 18 23 f1mpt ⊢ ( ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ) : ( 𝑌 𝐻 𝑧 ) –1-1→ ( 𝑋 𝐻 𝑧 ) ↔ ( ∀ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑧 ) ∧ ∀ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ∀ ℎ ∈ ( 𝑌 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) = ( ℎ ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) → 𝑔 = ℎ ) ) )
25 24 baib ⊢ ( ∀ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑧 ) → ( ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ) : ( 𝑌 𝐻 𝑧 ) –1-1→ ( 𝑋 𝐻 𝑧 ) ↔ ∀ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ∀ ℎ ∈ ( 𝑌 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) = ( ℎ ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) → 𝑔 = ℎ ) ) )
26 22 25 bitr3d ⊢ ( ∀ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑧 ) → ( Fun ◡ ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ) ↔ ∀ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ∀ ℎ ∈ ( 𝑌 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) = ( ℎ ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) → 𝑔 = ℎ ) ) )
27 17 26 syl ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( Fun ◡ ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ) ↔ ∀ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ∀ ℎ ∈ ( 𝑌 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) = ( ℎ ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) → 𝑔 = ℎ ) ) )
28 27 ralbidva ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( ∀ 𝑧 ∈ 𝐵 Fun ◡ ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ) ↔ ∀ 𝑧 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ∀ ℎ ∈ ( 𝑌 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) = ( ℎ ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) → 𝑔 = ℎ ) ) )
29 28 pm5.32da ⊢ ( 𝜑 → ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∀ 𝑧 ∈ 𝐵 Fun ◡ ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ) ) ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ∀ ℎ ∈ ( 𝑌 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) = ( ℎ ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) → 𝑔 = ℎ ) ) ) )
30 8 29 bitrd ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ∀ ℎ ∈ ( 𝑌 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) = ( ℎ ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) → 𝑔 = ℎ ) ) ) )