Step | Hyp | Ref
| Expression |
1 | | funcsetcestrc.s |
. . 3
⊢ 𝑆 = (SetCat‘𝑈) |
2 | | funcsetcestrc.c |
. . 3
⊢ 𝐶 = (Base‘𝑆) |
3 | | funcsetcestrc.f |
. . 3
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) |
4 | | funcsetcestrc.u |
. . 3
⊢ (𝜑 → 𝑈 ∈ WUni) |
5 | | funcsetcestrc.o |
. . 3
⊢ (𝜑 → ω ∈ 𝑈) |
6 | | funcsetcestrc.g |
. . 3
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥)))) |
7 | | funcsetcestrc.e |
. . 3
⊢ 𝐸 = (ExtStrCat‘𝑈) |
8 | 1, 2, 3, 4, 5, 6, 7 | funcsetcestrc 17881 |
. 2
⊢ (𝜑 → 𝐹(𝑆 Func 𝐸)𝐺) |
9 | 1, 2, 3, 4, 5, 6, 7 | funcsetcestrclem8 17879 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (𝑎𝐺𝑏):(𝑎(Hom ‘𝑆)𝑏)⟶((𝐹‘𝑎)(Hom ‘𝐸)(𝐹‘𝑏))) |
10 | 4 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → 𝑈 ∈ WUni) |
11 | | eqid 2738 |
. . . . . . 7
⊢ (Hom
‘𝐸) = (Hom
‘𝐸) |
12 | 1, 2, 3, 4, 5 | funcsetcestrclem2 17872 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → (𝐹‘𝑎) ∈ 𝑈) |
13 | 12 | adantrr 714 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (𝐹‘𝑎) ∈ 𝑈) |
14 | 1, 2, 3, 4, 5 | funcsetcestrclem2 17872 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐶) → (𝐹‘𝑏) ∈ 𝑈) |
15 | 14 | adantrl 713 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (𝐹‘𝑏) ∈ 𝑈) |
16 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘(𝐹‘𝑎)) = (Base‘(𝐹‘𝑎)) |
17 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘(𝐹‘𝑏)) = (Base‘(𝐹‘𝑏)) |
18 | 7, 10, 11, 13, 15, 16, 17 | elestrchom 17844 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (ℎ ∈ ((𝐹‘𝑎)(Hom ‘𝐸)(𝐹‘𝑏)) ↔ ℎ:(Base‘(𝐹‘𝑎))⟶(Base‘(𝐹‘𝑏)))) |
19 | 1, 2, 3 | funcsetcestrclem1 17871 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → (𝐹‘𝑎) = {〈(Base‘ndx), 𝑎〉}) |
20 | 19 | adantrr 714 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (𝐹‘𝑎) = {〈(Base‘ndx), 𝑎〉}) |
21 | 20 | fveq2d 6778 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (Base‘(𝐹‘𝑎)) = (Base‘{〈(Base‘ndx),
𝑎〉})) |
22 | | eqid 2738 |
. . . . . . . . . . 11
⊢
{〈(Base‘ndx), 𝑎〉} = {〈(Base‘ndx), 𝑎〉} |
23 | 22 | 1strbas 16929 |
. . . . . . . . . 10
⊢ (𝑎 ∈ 𝐶 → 𝑎 = (Base‘{〈(Base‘ndx), 𝑎〉})) |
24 | 23 | ad2antrl 725 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → 𝑎 = (Base‘{〈(Base‘ndx), 𝑎〉})) |
25 | 21, 24 | eqtr4d 2781 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (Base‘(𝐹‘𝑎)) = 𝑎) |
26 | 1, 2, 3 | funcsetcestrclem1 17871 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐶) → (𝐹‘𝑏) = {〈(Base‘ndx), 𝑏〉}) |
27 | 26 | adantrl 713 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (𝐹‘𝑏) = {〈(Base‘ndx), 𝑏〉}) |
28 | 27 | fveq2d 6778 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (Base‘(𝐹‘𝑏)) = (Base‘{〈(Base‘ndx),
𝑏〉})) |
29 | | eqid 2738 |
. . . . . . . . . . 11
⊢
{〈(Base‘ndx), 𝑏〉} = {〈(Base‘ndx), 𝑏〉} |
30 | 29 | 1strbas 16929 |
. . . . . . . . . 10
⊢ (𝑏 ∈ 𝐶 → 𝑏 = (Base‘{〈(Base‘ndx), 𝑏〉})) |
31 | 30 | ad2antll 726 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → 𝑏 = (Base‘{〈(Base‘ndx), 𝑏〉})) |
32 | 28, 31 | eqtr4d 2781 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (Base‘(𝐹‘𝑏)) = 𝑏) |
33 | 25, 32 | feq23d 6595 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (ℎ:(Base‘(𝐹‘𝑎))⟶(Base‘(𝐹‘𝑏)) ↔ ℎ:𝑎⟶𝑏)) |
34 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) |
35 | 34 | ancomd 462 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (𝑏 ∈ 𝐶 ∧ 𝑎 ∈ 𝐶)) |
36 | | elmapg 8628 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ 𝐶 ∧ 𝑎 ∈ 𝐶) → (ℎ ∈ (𝑏 ↑m 𝑎) ↔ ℎ:𝑎⟶𝑏)) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (ℎ ∈ (𝑏 ↑m 𝑎) ↔ ℎ:𝑎⟶𝑏)) |
38 | 37 | biimpar 478 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) ∧ ℎ:𝑎⟶𝑏) → ℎ ∈ (𝑏 ↑m 𝑎)) |
39 | | equequ2 2029 |
. . . . . . . . . . . 12
⊢ (𝑘 = ℎ → (ℎ = 𝑘 ↔ ℎ = ℎ)) |
40 | 39 | adantl 482 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) ∧ ℎ:𝑎⟶𝑏) ∧ 𝑘 = ℎ) → (ℎ = 𝑘 ↔ ℎ = ℎ)) |
41 | | eqidd 2739 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) ∧ ℎ:𝑎⟶𝑏) → ℎ = ℎ) |
42 | 38, 40, 41 | rspcedvd 3563 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) ∧ ℎ:𝑎⟶𝑏) → ∃𝑘 ∈ (𝑏 ↑m 𝑎)ℎ = 𝑘) |
43 | 1, 2, 3, 4, 5, 6 | funcsetcestrclem6 17877 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶) ∧ 𝑘 ∈ (𝑏 ↑m 𝑎)) → ((𝑎𝐺𝑏)‘𝑘) = 𝑘) |
44 | 43 | 3expa 1117 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) ∧ 𝑘 ∈ (𝑏 ↑m 𝑎)) → ((𝑎𝐺𝑏)‘𝑘) = 𝑘) |
45 | 44 | eqeq2d 2749 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) ∧ 𝑘 ∈ (𝑏 ↑m 𝑎)) → (ℎ = ((𝑎𝐺𝑏)‘𝑘) ↔ ℎ = 𝑘)) |
46 | 45 | rexbidva 3225 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (∃𝑘 ∈ (𝑏 ↑m 𝑎)ℎ = ((𝑎𝐺𝑏)‘𝑘) ↔ ∃𝑘 ∈ (𝑏 ↑m 𝑎)ℎ = 𝑘)) |
47 | 46 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) ∧ ℎ:𝑎⟶𝑏) → (∃𝑘 ∈ (𝑏 ↑m 𝑎)ℎ = ((𝑎𝐺𝑏)‘𝑘) ↔ ∃𝑘 ∈ (𝑏 ↑m 𝑎)ℎ = 𝑘)) |
48 | 42, 47 | mpbird 256 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) ∧ ℎ:𝑎⟶𝑏) → ∃𝑘 ∈ (𝑏 ↑m 𝑎)ℎ = ((𝑎𝐺𝑏)‘𝑘)) |
49 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ (Hom
‘𝑆) = (Hom
‘𝑆) |
50 | 1, 4 | setcbas 17793 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑈 = (Base‘𝑆)) |
51 | 2, 50 | eqtr4id 2797 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 = 𝑈) |
52 | 51 | eleq2d 2824 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑎 ∈ 𝐶 ↔ 𝑎 ∈ 𝑈)) |
53 | 52 | biimpcd 248 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ 𝐶 → (𝜑 → 𝑎 ∈ 𝑈)) |
54 | 53 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶) → (𝜑 → 𝑎 ∈ 𝑈)) |
55 | 54 | impcom 408 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → 𝑎 ∈ 𝑈) |
56 | 51 | eleq2d 2824 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑏 ∈ 𝐶 ↔ 𝑏 ∈ 𝑈)) |
57 | 56 | biimpcd 248 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ 𝐶 → (𝜑 → 𝑏 ∈ 𝑈)) |
58 | 57 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶) → (𝜑 → 𝑏 ∈ 𝑈)) |
59 | 58 | impcom 408 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → 𝑏 ∈ 𝑈) |
60 | 1, 10, 49, 55, 59 | setchom 17795 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (𝑎(Hom ‘𝑆)𝑏) = (𝑏 ↑m 𝑎)) |
61 | 60 | rexeqdv 3349 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (∃𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏)ℎ = ((𝑎𝐺𝑏)‘𝑘) ↔ ∃𝑘 ∈ (𝑏 ↑m 𝑎)ℎ = ((𝑎𝐺𝑏)‘𝑘))) |
62 | 61 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) ∧ ℎ:𝑎⟶𝑏) → (∃𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏)ℎ = ((𝑎𝐺𝑏)‘𝑘) ↔ ∃𝑘 ∈ (𝑏 ↑m 𝑎)ℎ = ((𝑎𝐺𝑏)‘𝑘))) |
63 | 48, 62 | mpbird 256 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) ∧ ℎ:𝑎⟶𝑏) → ∃𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏)ℎ = ((𝑎𝐺𝑏)‘𝑘)) |
64 | 63 | ex 413 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (ℎ:𝑎⟶𝑏 → ∃𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏)ℎ = ((𝑎𝐺𝑏)‘𝑘))) |
65 | 33, 64 | sylbid 239 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (ℎ:(Base‘(𝐹‘𝑎))⟶(Base‘(𝐹‘𝑏)) → ∃𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏)ℎ = ((𝑎𝐺𝑏)‘𝑘))) |
66 | 18, 65 | sylbid 239 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (ℎ ∈ ((𝐹‘𝑎)(Hom ‘𝐸)(𝐹‘𝑏)) → ∃𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏)ℎ = ((𝑎𝐺𝑏)‘𝑘))) |
67 | 66 | ralrimiv 3102 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → ∀ℎ ∈ ((𝐹‘𝑎)(Hom ‘𝐸)(𝐹‘𝑏))∃𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏)ℎ = ((𝑎𝐺𝑏)‘𝑘)) |
68 | | dffo3 6978 |
. . . 4
⊢ ((𝑎𝐺𝑏):(𝑎(Hom ‘𝑆)𝑏)–onto→((𝐹‘𝑎)(Hom ‘𝐸)(𝐹‘𝑏)) ↔ ((𝑎𝐺𝑏):(𝑎(Hom ‘𝑆)𝑏)⟶((𝐹‘𝑎)(Hom ‘𝐸)(𝐹‘𝑏)) ∧ ∀ℎ ∈ ((𝐹‘𝑎)(Hom ‘𝐸)(𝐹‘𝑏))∃𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏)ℎ = ((𝑎𝐺𝑏)‘𝑘))) |
69 | 9, 67, 68 | sylanbrc 583 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (𝑎𝐺𝑏):(𝑎(Hom ‘𝑆)𝑏)–onto→((𝐹‘𝑎)(Hom ‘𝐸)(𝐹‘𝑏))) |
70 | 69 | ralrimivva 3123 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐶 (𝑎𝐺𝑏):(𝑎(Hom ‘𝑆)𝑏)–onto→((𝐹‘𝑎)(Hom ‘𝐸)(𝐹‘𝑏))) |
71 | 2, 11, 49 | isfull2 17627 |
. 2
⊢ (𝐹(𝑆 Full 𝐸)𝐺 ↔ (𝐹(𝑆 Func 𝐸)𝐺 ∧ ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐶 (𝑎𝐺𝑏):(𝑎(Hom ‘𝑆)𝑏)–onto→((𝐹‘𝑎)(Hom ‘𝐸)(𝐹‘𝑏)))) |
72 | 8, 70, 71 | sylanbrc 583 |
1
⊢ (𝜑 → 𝐹(𝑆 Full 𝐸)𝐺) |