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 𝑆 ) 𝐺 )