Metamath Proof Explorer

Theorem fthmon

Description: A faithful functor reflects monomorphisms. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses fthmon.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
fthmon.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
fthmon.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 )
fthmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
fthmon.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
fthmon.r ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑋 𝐻 𝑌 ) )
fthmon.m ⊢ 𝑀 = ( Mono ‘ 𝐶 )
fthmon.n ⊢ 𝑁 = ( Mono ‘ 𝐷 )
fthmon.1 ⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝑁 ( 𝐹 ‘ 𝑌 ) ) )
Assertion fthmon ( 𝜑 → 𝑅 ∈ ( 𝑋 𝑀 𝑌 ) )

Proof

Step Hyp Ref Expression
1 fthmon.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 fthmon.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 fthmon.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 )
4 fthmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 fthmon.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 fthmon.r ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑋 𝐻 𝑌 ) )
7 fthmon.m ⊢ 𝑀 = ( Mono ‘ 𝐶 )
8 fthmon.n ⊢ 𝑁 = ( Mono ‘ 𝐷 )
9 fthmon.1 ⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝑁 ( 𝐹 ‘ 𝑌 ) ) )
10 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
11 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
12 eqid ⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
13 fthfunc ⊢ ( 𝐶 Faith 𝐷 ) ⊆ ( 𝐶 Func 𝐷 )
14 13 ssbri ⊢ ( 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
15 3 14 syl ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
16 df-br ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
17 15 16 sylib ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
18 funcrcl ⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
19 17 18 syl ⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
20 19 simprd ⊢ ( 𝜑 → 𝐷 ∈ Cat )
21 20 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝐷 ∈ Cat )
22 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
23 1 10 22 funcf1 ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
24 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝑋 ∈ 𝐵 )
25 23 24 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
26 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝑌 ∈ 𝐵 )
27 23 26 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ( 𝐹 ‘ 𝑌 ) ∈ ( Base ‘ 𝐷 ) )
28 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝑧 ∈ 𝐵 )
29 23 28 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ( Base ‘ 𝐷 ) )
30 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝑁 ( 𝐹 ‘ 𝑌 ) ) )
31 1 2 11 22 28 24 funcf2 ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ( 𝑧 𝐺 𝑋 ) : ( 𝑧 𝐻 𝑋 ) ⟶ ( ( 𝐹 ‘ 𝑧 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑋 ) ) )
32 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) )
33 31 32 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ( ( 𝑧 𝐺 𝑋 ) ‘ 𝑓 ) ∈ ( ( 𝐹 ‘ 𝑧 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑋 ) ) )
34 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) )
35 31 34 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ( ( 𝑧 𝐺 𝑋 ) ‘ 𝑔 ) ∈ ( ( 𝐹 ‘ 𝑧 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑋 ) ) )
36 10 11 12 8 21 25 27 29 30 33 35 moni ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ( ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ( ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑧 𝐺 𝑋 ) ‘ 𝑓 ) ) = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ( ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑧 𝐺 𝑋 ) ‘ 𝑔 ) ) ↔ ( ( 𝑧 𝐺 𝑋 ) ‘ 𝑓 ) = ( ( 𝑧 𝐺 𝑋 ) ‘ 𝑔 ) ) )
37 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
38 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝑅 ∈ ( 𝑋 𝐻 𝑌 ) )
39 1 2 37 12 22 28 24 26 32 38 funcco ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ( ( 𝑧 𝐺 𝑌 ) ‘ ( 𝑅 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑓 ) ) = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ( ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑧 𝐺 𝑋 ) ‘ 𝑓 ) ) )
40 1 2 37 12 22 28 24 26 34 38 funcco ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ( ( 𝑧 𝐺 𝑌 ) ‘ ( 𝑅 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) ) = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ( ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑧 𝐺 𝑋 ) ‘ 𝑔 ) ) )
41 39 40 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ( ( ( 𝑧 𝐺 𝑌 ) ‘ ( 𝑅 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑓 ) ) = ( ( 𝑧 𝐺 𝑌 ) ‘ ( 𝑅 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) ) ↔ ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ( ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑧 𝐺 𝑋 ) ‘ 𝑓 ) ) = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ( ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑧 𝐺 𝑋 ) ‘ 𝑔 ) ) ) )
42 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 )
43 19 simpld ⊢ ( 𝜑 → 𝐶 ∈ Cat )
44 43 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝐶 ∈ Cat )
45 1 2 37 44 28 24 26 32 38 catcocl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ( 𝑅 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑓 ) ∈ ( 𝑧 𝐻 𝑌 ) )
46 1 2 37 44 28 24 26 34 38 catcocl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ( 𝑅 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) ∈ ( 𝑧 𝐻 𝑌 ) )
47 1 2 11 42 28 26 45 46 fthi ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ( ( ( 𝑧 𝐺 𝑌 ) ‘ ( 𝑅 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑓 ) ) = ( ( 𝑧 𝐺 𝑌 ) ‘ ( 𝑅 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) ) ↔ ( 𝑅 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑓 ) = ( 𝑅 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) ) )
48 41 47 bitr3d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ( ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ( ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑧 𝐺 𝑋 ) ‘ 𝑓 ) ) = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ( ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑧 𝐺 𝑋 ) ‘ 𝑔 ) ) ↔ ( 𝑅 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑓 ) = ( 𝑅 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) ) )
49 1 2 11 42 28 24 32 34 fthi ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ( ( ( 𝑧 𝐺 𝑋 ) ‘ 𝑓 ) = ( ( 𝑧 𝐺 𝑋 ) ‘ 𝑔 ) ↔ 𝑓 = 𝑔 ) )
50 36 48 49 3bitr3d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ( ( 𝑅 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑓 ) = ( 𝑅 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) ↔ 𝑓 = 𝑔 ) )
51 50 biimpd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ( ( 𝑅 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑓 ) = ( 𝑅 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) → 𝑓 = 𝑔 ) )
52 51 ralrimivvva ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ( ( 𝑅 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑓 ) = ( 𝑅 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) → 𝑓 = 𝑔 ) )
53 1 2 37 7 43 4 5 ismon2 ⊢ ( 𝜑 → ( 𝑅 ∈ ( 𝑋 𝑀 𝑌 ) ↔ ( 𝑅 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑧 𝐻 𝑋 ) ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ( ( 𝑅 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑓 ) = ( 𝑅 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) → 𝑓 = 𝑔 ) ) ) )
54 6 52 53 mpbir2and ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑋 𝑀 𝑌 ) )