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 17671 |
. 2
⊢ (𝜑 → 𝐹(𝑆 Func 𝐸)𝐺) |
9 | 1, 2, 3, 4, 5, 6, 7 | funcsetcestrclem8 17669 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (𝑎𝐺𝑏):(𝑎(Hom ‘𝑆)𝑏)⟶((𝐹‘𝑎)(Hom ‘𝐸)(𝐹‘𝑏))) |
10 | 4 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → 𝑈 ∈ WUni) |
11 | | eqid 2737 |
. . . . . . 7
⊢ (Hom
‘𝐸) = (Hom
‘𝐸) |
12 | 1, 2, 3, 4, 5 | funcsetcestrclem2 17662 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → (𝐹‘𝑎) ∈ 𝑈) |
13 | 12 | adantrr 717 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (𝐹‘𝑎) ∈ 𝑈) |
14 | 1, 2, 3, 4, 5 | funcsetcestrclem2 17662 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐶) → (𝐹‘𝑏) ∈ 𝑈) |
15 | 14 | adantrl 716 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (𝐹‘𝑏) ∈ 𝑈) |
16 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘(𝐹‘𝑎)) = (Base‘(𝐹‘𝑎)) |
17 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘(𝐹‘𝑏)) = (Base‘(𝐹‘𝑏)) |
18 | 7, 10, 11, 13, 15, 16, 17 | elestrchom 17635 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (ℎ ∈ ((𝐹‘𝑎)(Hom ‘𝐸)(𝐹‘𝑏)) ↔ ℎ:(Base‘(𝐹‘𝑎))⟶(Base‘(𝐹‘𝑏)))) |
19 | 1, 2, 3 | funcsetcestrclem1 17661 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → (𝐹‘𝑎) = {〈(Base‘ndx), 𝑎〉}) |
20 | 19 | adantrr 717 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (𝐹‘𝑎) = {〈(Base‘ndx), 𝑎〉}) |
21 | 20 | fveq2d 6721 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (Base‘(𝐹‘𝑎)) = (Base‘{〈(Base‘ndx),
𝑎〉})) |
22 | | eqid 2737 |
. . . . . . . . . . 11
⊢
{〈(Base‘ndx), 𝑎〉} = {〈(Base‘ndx), 𝑎〉} |
23 | 22 | 1strbas 16775 |
. . . . . . . . . 10
⊢ (𝑎 ∈ 𝐶 → 𝑎 = (Base‘{〈(Base‘ndx), 𝑎〉})) |
24 | 23 | ad2antrl 728 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → 𝑎 = (Base‘{〈(Base‘ndx), 𝑎〉})) |
25 | 21, 24 | eqtr4d 2780 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (Base‘(𝐹‘𝑎)) = 𝑎) |
26 | 1, 2, 3 | funcsetcestrclem1 17661 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐶) → (𝐹‘𝑏) = {〈(Base‘ndx), 𝑏〉}) |
27 | 26 | adantrl 716 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (𝐹‘𝑏) = {〈(Base‘ndx), 𝑏〉}) |
28 | 27 | fveq2d 6721 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (Base‘(𝐹‘𝑏)) = (Base‘{〈(Base‘ndx),
𝑏〉})) |
29 | | eqid 2737 |
. . . . . . . . . . 11
⊢
{〈(Base‘ndx), 𝑏〉} = {〈(Base‘ndx), 𝑏〉} |
30 | 29 | 1strbas 16775 |
. . . . . . . . . 10
⊢ (𝑏 ∈ 𝐶 → 𝑏 = (Base‘{〈(Base‘ndx), 𝑏〉})) |
31 | 30 | ad2antll 729 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → 𝑏 = (Base‘{〈(Base‘ndx), 𝑏〉})) |
32 | 28, 31 | eqtr4d 2780 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (Base‘(𝐹‘𝑏)) = 𝑏) |
33 | 25, 32 | feq23d 6540 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (ℎ:(Base‘(𝐹‘𝑎))⟶(Base‘(𝐹‘𝑏)) ↔ ℎ:𝑎⟶𝑏)) |
34 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) |
35 | 34 | ancomd 465 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (𝑏 ∈ 𝐶 ∧ 𝑎 ∈ 𝐶)) |
36 | | elmapg 8521 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ 𝐶 ∧ 𝑎 ∈ 𝐶) → (ℎ ∈ (𝑏 ↑m 𝑎) ↔ ℎ:𝑎⟶𝑏)) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (ℎ ∈ (𝑏 ↑m 𝑎) ↔ ℎ:𝑎⟶𝑏)) |
38 | 37 | biimpar 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) ∧ ℎ:𝑎⟶𝑏) → ℎ ∈ (𝑏 ↑m 𝑎)) |
39 | | equequ2 2034 |
. . . . . . . . . . . 12
⊢ (𝑘 = ℎ → (ℎ = 𝑘 ↔ ℎ = ℎ)) |
40 | 39 | adantl 485 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) ∧ ℎ:𝑎⟶𝑏) ∧ 𝑘 = ℎ) → (ℎ = 𝑘 ↔ ℎ = ℎ)) |
41 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) ∧ ℎ:𝑎⟶𝑏) → ℎ = ℎ) |
42 | 38, 40, 41 | rspcedvd 3540 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) ∧ ℎ:𝑎⟶𝑏) → ∃𝑘 ∈ (𝑏 ↑m 𝑎)ℎ = 𝑘) |
43 | 1, 2, 3, 4, 5, 6 | funcsetcestrclem6 17667 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶) ∧ 𝑘 ∈ (𝑏 ↑m 𝑎)) → ((𝑎𝐺𝑏)‘𝑘) = 𝑘) |
44 | 43 | 3expa 1120 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) ∧ 𝑘 ∈ (𝑏 ↑m 𝑎)) → ((𝑎𝐺𝑏)‘𝑘) = 𝑘) |
45 | 44 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) ∧ 𝑘 ∈ (𝑏 ↑m 𝑎)) → (ℎ = ((𝑎𝐺𝑏)‘𝑘) ↔ ℎ = 𝑘)) |
46 | 45 | rexbidva 3215 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (∃𝑘 ∈ (𝑏 ↑m 𝑎)ℎ = ((𝑎𝐺𝑏)‘𝑘) ↔ ∃𝑘 ∈ (𝑏 ↑m 𝑎)ℎ = 𝑘)) |
47 | 46 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) ∧ ℎ:𝑎⟶𝑏) → (∃𝑘 ∈ (𝑏 ↑m 𝑎)ℎ = ((𝑎𝐺𝑏)‘𝑘) ↔ ∃𝑘 ∈ (𝑏 ↑m 𝑎)ℎ = 𝑘)) |
48 | 42, 47 | mpbird 260 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) ∧ ℎ:𝑎⟶𝑏) → ∃𝑘 ∈ (𝑏 ↑m 𝑎)ℎ = ((𝑎𝐺𝑏)‘𝑘)) |
49 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (Hom
‘𝑆) = (Hom
‘𝑆) |
50 | 1, 4 | setcbas 17584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑈 = (Base‘𝑆)) |
51 | 2, 50 | eqtr4id 2797 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 = 𝑈) |
52 | 51 | eleq2d 2823 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑎 ∈ 𝐶 ↔ 𝑎 ∈ 𝑈)) |
53 | 52 | biimpcd 252 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ 𝐶 → (𝜑 → 𝑎 ∈ 𝑈)) |
54 | 53 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶) → (𝜑 → 𝑎 ∈ 𝑈)) |
55 | 54 | impcom 411 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → 𝑎 ∈ 𝑈) |
56 | 51 | eleq2d 2823 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑏 ∈ 𝐶 ↔ 𝑏 ∈ 𝑈)) |
57 | 56 | biimpcd 252 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ 𝐶 → (𝜑 → 𝑏 ∈ 𝑈)) |
58 | 57 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶) → (𝜑 → 𝑏 ∈ 𝑈)) |
59 | 58 | impcom 411 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → 𝑏 ∈ 𝑈) |
60 | 1, 10, 49, 55, 59 | setchom 17586 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (𝑎(Hom ‘𝑆)𝑏) = (𝑏 ↑m 𝑎)) |
61 | 60 | rexeqdv 3326 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (∃𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏)ℎ = ((𝑎𝐺𝑏)‘𝑘) ↔ ∃𝑘 ∈ (𝑏 ↑m 𝑎)ℎ = ((𝑎𝐺𝑏)‘𝑘))) |
62 | 61 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) ∧ ℎ:𝑎⟶𝑏) → (∃𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏)ℎ = ((𝑎𝐺𝑏)‘𝑘) ↔ ∃𝑘 ∈ (𝑏 ↑m 𝑎)ℎ = ((𝑎𝐺𝑏)‘𝑘))) |
63 | 48, 62 | mpbird 260 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) ∧ ℎ:𝑎⟶𝑏) → ∃𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏)ℎ = ((𝑎𝐺𝑏)‘𝑘)) |
64 | 63 | ex 416 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (ℎ:𝑎⟶𝑏 → ∃𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏)ℎ = ((𝑎𝐺𝑏)‘𝑘))) |
65 | 33, 64 | sylbid 243 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (ℎ:(Base‘(𝐹‘𝑎))⟶(Base‘(𝐹‘𝑏)) → ∃𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏)ℎ = ((𝑎𝐺𝑏)‘𝑘))) |
66 | 18, 65 | sylbid 243 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (ℎ ∈ ((𝐹‘𝑎)(Hom ‘𝐸)(𝐹‘𝑏)) → ∃𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏)ℎ = ((𝑎𝐺𝑏)‘𝑘))) |
67 | 66 | ralrimiv 3104 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → ∀ℎ ∈ ((𝐹‘𝑎)(Hom ‘𝐸)(𝐹‘𝑏))∃𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏)ℎ = ((𝑎𝐺𝑏)‘𝑘)) |
68 | | dffo3 6921 |
. . . 4
⊢ ((𝑎𝐺𝑏):(𝑎(Hom ‘𝑆)𝑏)–onto→((𝐹‘𝑎)(Hom ‘𝐸)(𝐹‘𝑏)) ↔ ((𝑎𝐺𝑏):(𝑎(Hom ‘𝑆)𝑏)⟶((𝐹‘𝑎)(Hom ‘𝐸)(𝐹‘𝑏)) ∧ ∀ℎ ∈ ((𝐹‘𝑎)(Hom ‘𝐸)(𝐹‘𝑏))∃𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏)ℎ = ((𝑎𝐺𝑏)‘𝑘))) |
69 | 9, 67, 68 | sylanbrc 586 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (𝑎𝐺𝑏):(𝑎(Hom ‘𝑆)𝑏)–onto→((𝐹‘𝑎)(Hom ‘𝐸)(𝐹‘𝑏))) |
70 | 69 | ralrimivva 3112 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐶 (𝑎𝐺𝑏):(𝑎(Hom ‘𝑆)𝑏)–onto→((𝐹‘𝑎)(Hom ‘𝐸)(𝐹‘𝑏))) |
71 | 2, 11, 49 | isfull2 17418 |
. 2
⊢ (𝐹(𝑆 Full 𝐸)𝐺 ↔ (𝐹(𝑆 Func 𝐸)𝐺 ∧ ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐶 (𝑎𝐺𝑏):(𝑎(Hom ‘𝑆)𝑏)–onto→((𝐹‘𝑎)(Hom ‘𝐸)(𝐹‘𝑏)))) |
72 | 8, 70, 71 | sylanbrc 586 |
1
⊢ (𝜑 → 𝐹(𝑆 Full 𝐸)𝐺) |