Metamath Proof Explorer

Theorem fthestrcsetc

Description: The "natural forgetful functor" from the category of extensible structures into the category of sets which sends each extensible structure to its base set is faithful. (Contributed by AV, 2-Apr-2020)

Ref Expression
Hypotheses funcestrcsetc.e ⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
funcestrcsetc.s ⊢ 𝑆 = ( SetCat ‘ 𝑈 )
funcestrcsetc.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
funcestrcsetc.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
funcestrcsetc.u ⊢ ( 𝜑 → 𝑈 ∈ WUni )
funcestrcsetc.f ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( Base ‘ 𝑥 ) ) )
funcestrcsetc.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) )
Assertion fthestrcsetc ( 𝜑 → 𝐹 ( 𝐸 Faith 𝑆 ) 𝐺 )

Proof

Step Hyp Ref Expression
1 funcestrcsetc.e ⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
2 funcestrcsetc.s ⊢ 𝑆 = ( SetCat ‘ 𝑈 )
3 funcestrcsetc.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
4 funcestrcsetc.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
5 funcestrcsetc.u ⊢ ( 𝜑 → 𝑈 ∈ WUni )
6 funcestrcsetc.f ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( Base ‘ 𝑥 ) ) )
7 funcestrcsetc.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) )
8 1 2 3 4 5 6 7 funcestrcsetc ⊢ ( 𝜑 → 𝐹 ( 𝐸 Func 𝑆 ) 𝐺 )
9 1 2 3 4 5 6 7 funcestrcsetclem8 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) ⟶ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) )
10 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑈 ∈ WUni )
11 eqid ⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
12 1 5 estrcbas ⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝐸 ) )
13 3 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 eqid ⊢ ( Base ‘ 𝑎 ) = ( Base ‘ 𝑎 )
23 eqid ⊢ ( Base ‘ 𝑏 ) = ( Base ‘ 𝑏 )
24 1 10 11 17 21 22 23 estrchom ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) = ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) )
25 24 eleq2d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ℎ ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) ↔ ℎ ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) )
26 1 2 3 4 5 6 7 22 23 funcestrcsetclem6 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ℎ ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) → ( ( 𝑎 𝐺 𝑏 ) ‘ ℎ ) = ℎ )
27 26 3expia ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ℎ ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) → ( ( 𝑎 𝐺 𝑏 ) ‘ ℎ ) = ℎ ) )
28 25 27 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ℎ ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) → ( ( 𝑎 𝐺 𝑏 ) ‘ ℎ ) = ℎ ) )
29 28 com12 ⊢ ( ℎ ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) → ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑎 𝐺 𝑏 ) ‘ ℎ ) = ℎ ) )
30 29 adantr ⊢ ( ( ℎ ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) ∧ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) ) → ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑎 𝐺 𝑏 ) ‘ ℎ ) = ℎ ) )
31 30 impcom ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( ℎ ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) ∧ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) ) ) → ( ( 𝑎 𝐺 𝑏 ) ‘ ℎ ) = ℎ )
32 24 eleq2d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) ↔ 𝑘 ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) )
33 1 2 3 4 5 6 7 22 23 funcestrcsetclem6 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) → ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) = 𝑘 )
34 33 3expia ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑘 ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) → ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) = 𝑘 ) )
35 32 34 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) → ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) = 𝑘 ) )
36 35 com12 ⊢ ( 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) → ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) = 𝑘 ) )
37 36 adantl ⊢ ( ( ℎ ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) ∧ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) ) → ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) = 𝑘 ) )
38 37 impcom ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( ℎ ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) ∧ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) ) ) → ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) = 𝑘 )
39 31 38 eqeq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( ℎ ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) ∧ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) ) ) → ( ( ( 𝑎 𝐺 𝑏 ) ‘ ℎ ) = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) ↔ ℎ = 𝑘 ) )
40 39 biimpd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( ℎ ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) ∧ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) ) ) → ( ( ( 𝑎 𝐺 𝑏 ) ‘ ℎ ) = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) → ℎ = 𝑘 ) )
41 40 ralrimivva ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ∀ ℎ ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) ∀ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) ( ( ( 𝑎 𝐺 𝑏 ) ‘ ℎ ) = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) → ℎ = 𝑘 ) )
42 dff13 ⊢ ( ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) –1-1→ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) ↔ ( ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) ⟶ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) ∧ ∀ ℎ ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) ∀ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) ( ( ( 𝑎 𝐺 𝑏 ) ‘ ℎ ) = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) → ℎ = 𝑘 ) ) )
43 9 41 42 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) –1-1→ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) )
44 43 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) –1-1→ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) )
45 eqid ⊢ ( Hom ‘ 𝑆 ) = ( Hom ‘ 𝑆 )
46 3 11 45 isfth2 ⊢ ( 𝐹 ( 𝐸 Faith 𝑆 ) 𝐺 ↔ ( 𝐹 ( 𝐸 Func 𝑆 ) 𝐺 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) –1-1→ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) ) )
47 8 44 46 sylanbrc ⊢ ( 𝜑 → 𝐹 ( 𝐸 Faith 𝑆 ) 𝐺 )