Metamath Proof Explorer

Theorem fthsetcestrc

Description: The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only is faithful. (Contributed by AV, 31-Mar-2020)

Ref Expression
Hypotheses funcsetcestrc.s ⊢ 𝑆 = ( SetCat ‘ 𝑈 )
funcsetcestrc.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
funcsetcestrc.f ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐶 ↦ { ⟨ ( Base ‘ ndx ) , 𝑥 ⟩ } ) )
funcsetcestrc.u ⊢ ( 𝜑 → 𝑈 ∈ WUni )
funcsetcestrc.o ⊢ ( 𝜑 → ω ∈ 𝑈 )
funcsetcestrc.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐶 ↦ ( I ↾ ( 𝑦 ↑m 𝑥 ) ) ) )
funcsetcestrc.e ⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
Assertion fthsetcestrc ( 𝜑 → 𝐹 ( 𝑆 Faith 𝐸 ) 𝐺 )

Proof

Step Hyp Ref Expression
1 funcsetcestrc.s ⊢ 𝑆 = ( SetCat ‘ 𝑈 )
2 funcsetcestrc.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
3 funcsetcestrc.f ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐶 ↦ { ⟨ ( Base ‘ ndx ) , 𝑥 ⟩ } ) )
4 funcsetcestrc.u ⊢ ( 𝜑 → 𝑈 ∈ WUni )
5 funcsetcestrc.o ⊢ ( 𝜑 → ω ∈ 𝑈 )
6 funcsetcestrc.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐶 ↦ ( I ↾ ( 𝑦 ↑m 𝑥 ) ) ) )
7 funcsetcestrc.e ⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
8 1 2 3 4 5 6 7 funcsetcestrc ⊢ ( 𝜑 → 𝐹 ( 𝑆 Func 𝐸 ) 𝐺 )
9 1 2 3 4 5 6 7 funcsetcestrclem8 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ⟶ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑏 ) ) )
10 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → 𝑈 ∈ WUni )
11 eqid ⊢ ( Hom ‘ 𝑆 ) = ( Hom ‘ 𝑆 )
12 1 4 setcbas ⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝑆 ) )
13 2 12 eqtr4id ⊢ ( 𝜑 → 𝐶 = 𝑈 )
14 13 eleq2d ⊢ ( 𝜑 → ( 𝑎 ∈ 𝐶 ↔ 𝑎 ∈ 𝑈 ) )
15 14 biimpcd ⊢ ( 𝑎 ∈ 𝐶 → ( 𝜑 → 𝑎 ∈ 𝑈 ) )
16 15 adantr ⊢ ( ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) → ( 𝜑 → 𝑎 ∈ 𝑈 ) )
17 16 impcom ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → 𝑎 ∈ 𝑈 )
18 13 eleq2d ⊢ ( 𝜑 → ( 𝑏 ∈ 𝐶 ↔ 𝑏 ∈ 𝑈 ) )
19 18 biimpcd ⊢ ( 𝑏 ∈ 𝐶 → ( 𝜑 → 𝑏 ∈ 𝑈 ) )
20 19 adantl ⊢ ( ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) → ( 𝜑 → 𝑏 ∈ 𝑈 ) )
21 20 impcom ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → 𝑏 ∈ 𝑈 )
22 1 10 11 17 21 setchom ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) = ( 𝑏 ↑m 𝑎 ) )
23 22 eleq2d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( ℎ ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ↔ ℎ ∈ ( 𝑏 ↑m 𝑎 ) ) )
24 1 2 3 4 5 6 funcsetcestrclem6 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ∧ ℎ ∈ ( 𝑏 ↑m 𝑎 ) ) → ( ( 𝑎 𝐺 𝑏 ) ‘ ℎ ) = ℎ )
25 24 3expia ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( ℎ ∈ ( 𝑏 ↑m 𝑎 ) → ( ( 𝑎 𝐺 𝑏 ) ‘ ℎ ) = ℎ ) )
26 23 25 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( ℎ ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) → ( ( 𝑎 𝐺 𝑏 ) ‘ ℎ ) = ℎ ) )
27 26 com12 ⊢ ( ℎ ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) → ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( ( 𝑎 𝐺 𝑏 ) ‘ ℎ ) = ℎ ) )
28 27 adantr ⊢ ( ( ℎ ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ∧ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ) → ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( ( 𝑎 𝐺 𝑏 ) ‘ ℎ ) = ℎ ) )
29 28 impcom ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) ∧ ( ℎ ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ∧ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ) ) → ( ( 𝑎 𝐺 𝑏 ) ‘ ℎ ) = ℎ )
30 22 eleq2d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ↔ 𝑘 ∈ ( 𝑏 ↑m 𝑎 ) ) )
31 1 2 3 4 5 6 funcsetcestrclem6 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑘 ∈ ( 𝑏 ↑m 𝑎 ) ) → ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) = 𝑘 )
32 31 3expia ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( 𝑘 ∈ ( 𝑏 ↑m 𝑎 ) → ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) = 𝑘 ) )
33 30 32 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) → ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) = 𝑘 ) )
34 33 com12 ⊢ ( 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) → ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) = 𝑘 ) )
35 34 adantl ⊢ ( ( ℎ ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ∧ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ) → ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) = 𝑘 ) )
36 35 impcom ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) ∧ ( ℎ ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ∧ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ) ) → ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) = 𝑘 )
37 29 36 eqeq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) ∧ ( ℎ ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ∧ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ) ) → ( ( ( 𝑎 𝐺 𝑏 ) ‘ ℎ ) = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) ↔ ℎ = 𝑘 ) )
38 37 biimpd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) ∧ ( ℎ ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ∧ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ) ) → ( ( ( 𝑎 𝐺 𝑏 ) ‘ ℎ ) = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) → ℎ = 𝑘 ) )
39 38 ralrimivva ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ∀ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ∀ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ( ( ( 𝑎 𝐺 𝑏 ) ‘ ℎ ) = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) → ℎ = 𝑘 ) )
40 dff13 ⊢ ( ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) –1-1→ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑏 ) ) ↔ ( ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ⟶ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑏 ) ) ∧ ∀ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ∀ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ( ( ( 𝑎 𝐺 𝑏 ) ‘ ℎ ) = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) → ℎ = 𝑘 ) ) )
41 9 39 40 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) –1-1→ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑏 ) ) )
42 41 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐶 ∀ 𝑏 ∈ 𝐶 ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) –1-1→ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑏 ) ) )
43 eqid ⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
44 2 11 43 isfth2 ⊢ ( 𝐹 ( 𝑆 Faith 𝐸 ) 𝐺 ↔ ( 𝐹 ( 𝑆 Func 𝐸 ) 𝐺 ∧ ∀ 𝑎 ∈ 𝐶 ∀ 𝑏 ∈ 𝐶 ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) –1-1→ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑏 ) ) ) )
45 8 42 44 sylanbrc ⊢ ( 𝜑 → 𝐹 ( 𝑆 Faith 𝐸 ) 𝐺 )