This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem setcmon

Description: A monomorphism of sets is an injection. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses setcmon.c ⊢ 𝐶 = ( SetCat ‘ 𝑈 )
setcmon.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
setcmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
setcmon.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
setcmon.h ⊢ 𝑀 = ( Mono ‘ 𝐶 )
Assertion setcmon ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ↔ 𝐹 : 𝑋 –1-1→ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 setcmon.c ⊢ 𝐶 = ( SetCat ‘ 𝑈 )
2 setcmon.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3 setcmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
4 setcmon.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
5 setcmon.h ⊢ 𝑀 = ( Mono ‘ 𝐶 )
6 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
8 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
9 1 setccat ⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )
10 2 9 syl ⊢ ( 𝜑 → 𝐶 ∈ Cat )
11 1 2 setcbas ⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝐶 ) )
12 3 11 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
13 4 11 eleqtrd ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
14 6 7 8 5 10 12 13 monhom ⊢ ( 𝜑 → ( 𝑋 𝑀 𝑌 ) ⊆ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
15 14 sselda ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) → 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
16 1 2 7 3 4 elsetchom ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ↔ 𝐹 : 𝑋 ⟶ 𝑌 ) )
17 16 biimpa ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
18 15 17 syldan ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
19 simprr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
20 19 sneqd ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → { ( 𝐹 ‘ 𝑥 ) } = { ( 𝐹 ‘ 𝑦 ) } )
21 20 xpeq2d ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝑋 × { ( 𝐹 ‘ 𝑥 ) } ) = ( 𝑋 × { ( 𝐹 ‘ 𝑦 ) } ) )
22 18 adantr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
23 22 ffnd ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → 𝐹 Fn 𝑋 )
24 simprll ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → 𝑥 ∈ 𝑋 )
25 fcoconst ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ∘ ( 𝑋 × { 𝑥 } ) ) = ( 𝑋 × { ( 𝐹 ‘ 𝑥 ) } ) )
26 23 24 25 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ∘ ( 𝑋 × { 𝑥 } ) ) = ( 𝑋 × { ( 𝐹 ‘ 𝑥 ) } ) )
27 simprlr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → 𝑦 ∈ 𝑋 )
28 fcoconst ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ∘ ( 𝑋 × { 𝑦 } ) ) = ( 𝑋 × { ( 𝐹 ‘ 𝑦 ) } ) )
29 23 27 28 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ∘ ( 𝑋 × { 𝑦 } ) ) = ( 𝑋 × { ( 𝐹 ‘ 𝑦 ) } ) )
30 21 26 29 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ∘ ( 𝑋 × { 𝑥 } ) ) = ( 𝐹 ∘ ( 𝑋 × { 𝑦 } ) ) )
31 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → 𝑈 ∈ 𝑉 )
32 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → 𝑋 ∈ 𝑈 )
33 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → 𝑌 ∈ 𝑈 )
34 fconst6g ⊢ ( 𝑥 ∈ 𝑋 → ( 𝑋 × { 𝑥 } ) : 𝑋 ⟶ 𝑋 )
35 24 34 syl ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝑋 × { 𝑥 } ) : 𝑋 ⟶ 𝑋 )
36 1 31 8 32 32 33 35 22 setcco ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( 𝑋 × { 𝑥 } ) ) = ( 𝐹 ∘ ( 𝑋 × { 𝑥 } ) ) )
37 fconst6g ⊢ ( 𝑦 ∈ 𝑋 → ( 𝑋 × { 𝑦 } ) : 𝑋 ⟶ 𝑋 )
38 27 37 syl ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝑋 × { 𝑦 } ) : 𝑋 ⟶ 𝑋 )
39 1 31 8 32 32 33 38 22 setcco ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( 𝑋 × { 𝑦 } ) ) = ( 𝐹 ∘ ( 𝑋 × { 𝑦 } ) ) )
40 30 36 39 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( 𝑋 × { 𝑥 } ) ) = ( 𝐹 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( 𝑋 × { 𝑦 } ) ) )
41 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → 𝐶 ∈ Cat )
42 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → 𝑋 ∈ ( Base ‘ 𝐶 ) )
43 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → 𝑌 ∈ ( Base ‘ 𝐶 ) )
44 simplr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) )
45 1 31 7 32 32 elsetchom ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝑋 × { 𝑥 } ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ↔ ( 𝑋 × { 𝑥 } ) : 𝑋 ⟶ 𝑋 ) )
46 35 45 mpbird ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝑋 × { 𝑥 } ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
47 1 31 7 32 32 elsetchom ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝑋 × { 𝑦 } ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ↔ ( 𝑋 × { 𝑦 } ) : 𝑋 ⟶ 𝑋 ) )
48 38 47 mpbird ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝑋 × { 𝑦 } ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
49 6 7 8 5 41 42 43 42 44 46 48 moni ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝐹 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( 𝑋 × { 𝑥 } ) ) = ( 𝐹 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( 𝑋 × { 𝑦 } ) ) ↔ ( 𝑋 × { 𝑥 } ) = ( 𝑋 × { 𝑦 } ) ) )
50 40 49 mpbid ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝑋 × { 𝑥 } ) = ( 𝑋 × { 𝑦 } ) )
51 50 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝑋 × { 𝑥 } ) ‘ 𝑥 ) = ( ( 𝑋 × { 𝑦 } ) ‘ 𝑥 ) )
52 vex ⊢ 𝑥 ∈ V
53 52 fvconst2 ⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝑋 × { 𝑥 } ) ‘ 𝑥 ) = 𝑥 )
54 24 53 syl ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝑋 × { 𝑥 } ) ‘ 𝑥 ) = 𝑥 )
55 vex ⊢ 𝑦 ∈ V
56 55 fvconst2 ⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝑋 × { 𝑦 } ) ‘ 𝑥 ) = 𝑦 )
57 24 56 syl ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝑋 × { 𝑦 } ) ‘ 𝑥 ) = 𝑦 )
58 51 54 57 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → 𝑥 = 𝑦 )
59 58 expr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
60 59 ralrimivva ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
61 dff13 ⊢ ( 𝐹 : 𝑋 –1-1→ 𝑌 ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
62 18 60 61 sylanbrc ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ) → 𝐹 : 𝑋 –1-1→ 𝑌 )
63 f1f ⊢ ( 𝐹 : 𝑋 –1-1→ 𝑌 → 𝐹 : 𝑋 ⟶ 𝑌 )
64 16 biimpar ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
65 63 64 sylan2 ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) → 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
66 11 adantr ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) → 𝑈 = ( Base ‘ 𝐶 ) )
67 66 eleq2d ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) → ( 𝑧 ∈ 𝑈 ↔ 𝑧 ∈ ( Base ‘ 𝐶 ) ) )
68 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) ) → 𝑈 ∈ 𝑉 )
69 simprl ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) ) → 𝑧 ∈ 𝑈 )
70 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) ) → 𝑋 ∈ 𝑈 )
71 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) ) → 𝑌 ∈ 𝑈 )
72 simprrl ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) ) → 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) )
73 1 68 7 69 70 elsetchom ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) ) → ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↔ 𝑔 : 𝑧 ⟶ 𝑋 ) )
74 72 73 mpbid ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) ) → 𝑔 : 𝑧 ⟶ 𝑋 )
75 63 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
76 1 68 8 69 70 71 74 75 setcco ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) ) → ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( 𝐹 ∘ 𝑔 ) )
77 simprrr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) ) → ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) )
78 1 68 7 69 70 elsetchom ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) ) → ( ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↔ ℎ : 𝑧 ⟶ 𝑋 ) )
79 77 78 mpbid ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) ) → ℎ : 𝑧 ⟶ 𝑋 )
80 1 68 8 69 70 71 79 75 setcco ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) ) → ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) = ( 𝐹 ∘ ℎ ) )
81 76 80 eqeq12d ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) ) → ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) ↔ ( 𝐹 ∘ 𝑔 ) = ( 𝐹 ∘ ℎ ) ) )
82 simplr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) ) → 𝐹 : 𝑋 –1-1→ 𝑌 )
83 cocan1 ⊢ ( ( 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝑔 : 𝑧 ⟶ 𝑋 ∧ ℎ : 𝑧 ⟶ 𝑋 ) → ( ( 𝐹 ∘ 𝑔 ) = ( 𝐹 ∘ ℎ ) ↔ 𝑔 = ℎ ) )
84 82 74 79 83 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) ) → ( ( 𝐹 ∘ 𝑔 ) = ( 𝐹 ∘ ℎ ) ↔ 𝑔 = ℎ ) )
85 84 biimpd ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) ) → ( ( 𝐹 ∘ 𝑔 ) = ( 𝐹 ∘ ℎ ) → 𝑔 = ℎ ) )
86 81 85 sylbid ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) ) → ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) → 𝑔 = ℎ ) )
87 86 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) → 𝑔 = ℎ ) )
88 87 ralrimivva ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ 𝑧 ∈ 𝑈 ) → ∀ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∀ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) → 𝑔 = ℎ ) )
89 88 ex ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) → ( 𝑧 ∈ 𝑈 → ∀ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∀ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) → 𝑔 = ℎ ) ) )
90 67 89 sylbird ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) → ( 𝑧 ∈ ( Base ‘ 𝐶 ) → ∀ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∀ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) → 𝑔 = ℎ ) ) )
91 90 ralrimiv ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) → ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∀ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) → 𝑔 = ℎ ) )
92 6 7 8 5 10 12 13 ismon2 ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∀ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) → 𝑔 = ℎ ) ) ) )
93 92 adantr ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) → ( 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∀ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) → 𝑔 = ℎ ) ) ) )
94 65 91 93 mpbir2and ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) → 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) )
95 62 94 impbida ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ↔ 𝐹 : 𝑋 –1-1→ 𝑌 ) )