| Step | Hyp | Ref
| Expression |
| 1 | | funcestrcsetc.e |
. . 3
⊢ 𝐸 = (ExtStrCat‘𝑈) |
| 2 | | funcestrcsetc.s |
. . 3
⊢ 𝑆 = (SetCat‘𝑈) |
| 3 | | funcestrcsetc.b |
. . 3
⊢ 𝐵 = (Base‘𝐸) |
| 4 | | funcestrcsetc.c |
. . 3
⊢ 𝐶 = (Base‘𝑆) |
| 5 | | funcestrcsetc.u |
. . 3
⊢ (𝜑 → 𝑈 ∈ WUni) |
| 6 | | funcestrcsetc.f |
. . 3
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) |
| 7 | | funcestrcsetc.g |
. . 3
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))) |
| 8 | 1, 2, 3, 4, 5, 6, 7 | funcestrcsetc 18194 |
. 2
⊢ (𝜑 → 𝐹(𝐸 Func 𝑆)𝐺) |
| 9 | 1, 2, 3, 4, 5, 6, 7 | funcestrcsetclem8 18192 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎𝐺𝑏):(𝑎(Hom ‘𝐸)𝑏)⟶((𝐹‘𝑎)(Hom ‘𝑆)(𝐹‘𝑏))) |
| 10 | 5 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑈 ∈ WUni) |
| 11 | | eqid 2737 |
. . . . . . . 8
⊢ (Hom
‘𝑆) = (Hom
‘𝑆) |
| 12 | 1, 2, 3, 4, 5, 6 | funcestrcsetclem2 18186 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝐹‘𝑎) ∈ 𝑈) |
| 13 | 12 | adantrr 717 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘𝑎) ∈ 𝑈) |
| 14 | 1, 2, 3, 4, 5, 6 | funcestrcsetclem2 18186 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹‘𝑏) ∈ 𝑈) |
| 15 | 14 | adantrl 716 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘𝑏) ∈ 𝑈) |
| 16 | 2, 10, 11, 13, 15 | elsetchom 18126 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (ℎ ∈ ((𝐹‘𝑎)(Hom ‘𝑆)(𝐹‘𝑏)) ↔ ℎ:(𝐹‘𝑎)⟶(𝐹‘𝑏))) |
| 17 | 1, 2, 3, 4, 5, 6 | funcestrcsetclem1 18185 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝐹‘𝑎) = (Base‘𝑎)) |
| 18 | 17 | adantrr 717 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘𝑎) = (Base‘𝑎)) |
| 19 | 1, 2, 3, 4, 5, 6 | funcestrcsetclem1 18185 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹‘𝑏) = (Base‘𝑏)) |
| 20 | 19 | adantrl 716 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘𝑏) = (Base‘𝑏)) |
| 21 | 18, 20 | feq23d 6731 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (ℎ:(𝐹‘𝑎)⟶(𝐹‘𝑏) ↔ ℎ:(Base‘𝑎)⟶(Base‘𝑏))) |
| 22 | 16, 21 | bitrd 279 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (ℎ ∈ ((𝐹‘𝑎)(Hom ‘𝑆)(𝐹‘𝑏)) ↔ ℎ:(Base‘𝑎)⟶(Base‘𝑏))) |
| 23 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑏)
∈ V |
| 24 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑎)
∈ V |
| 25 | 23, 24 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢
((Base‘𝑏)
∈ V ∧ (Base‘𝑎) ∈ V) |
| 26 | | elmapg 8879 |
. . . . . . . . . . . 12
⊢
(((Base‘𝑏)
∈ V ∧ (Base‘𝑎) ∈ V) → (ℎ ∈ ((Base‘𝑏) ↑m (Base‘𝑎)) ↔ ℎ:(Base‘𝑎)⟶(Base‘𝑏))) |
| 27 | 25, 26 | mp1i 13 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (ℎ ∈ ((Base‘𝑏) ↑m (Base‘𝑎)) ↔ ℎ:(Base‘𝑎)⟶(Base‘𝑏))) |
| 28 | 27 | biimpar 477 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ ℎ:(Base‘𝑎)⟶(Base‘𝑏)) → ℎ ∈ ((Base‘𝑏) ↑m (Base‘𝑎))) |
| 29 | | equequ2 2025 |
. . . . . . . . . . 11
⊢ (𝑘 = ℎ → (ℎ = 𝑘 ↔ ℎ = ℎ)) |
| 30 | 29 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ ℎ:(Base‘𝑎)⟶(Base‘𝑏)) ∧ 𝑘 = ℎ) → (ℎ = 𝑘 ↔ ℎ = ℎ)) |
| 31 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ ℎ:(Base‘𝑎)⟶(Base‘𝑏)) → ℎ = ℎ) |
| 32 | 28, 30, 31 | rspcedvd 3624 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ ℎ:(Base‘𝑎)⟶(Base‘𝑏)) → ∃𝑘 ∈ ((Base‘𝑏) ↑m (Base‘𝑎))ℎ = 𝑘) |
| 33 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑎) =
(Base‘𝑎) |
| 34 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑏) =
(Base‘𝑏) |
| 35 | 1, 2, 3, 4, 5, 6, 7, 33, 34 | funcestrcsetclem6 18190 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑘 ∈ ((Base‘𝑏) ↑m (Base‘𝑎))) → ((𝑎𝐺𝑏)‘𝑘) = 𝑘) |
| 36 | 35 | 3expa 1119 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑘 ∈ ((Base‘𝑏) ↑m (Base‘𝑎))) → ((𝑎𝐺𝑏)‘𝑘) = 𝑘) |
| 37 | 36 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑘 ∈ ((Base‘𝑏) ↑m (Base‘𝑎))) → (ℎ = ((𝑎𝐺𝑏)‘𝑘) ↔ ℎ = 𝑘)) |
| 38 | 37 | rexbidva 3177 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (∃𝑘 ∈ ((Base‘𝑏) ↑m (Base‘𝑎))ℎ = ((𝑎𝐺𝑏)‘𝑘) ↔ ∃𝑘 ∈ ((Base‘𝑏) ↑m (Base‘𝑎))ℎ = 𝑘)) |
| 39 | 38 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ ℎ:(Base‘𝑎)⟶(Base‘𝑏)) → (∃𝑘 ∈ ((Base‘𝑏) ↑m (Base‘𝑎))ℎ = ((𝑎𝐺𝑏)‘𝑘) ↔ ∃𝑘 ∈ ((Base‘𝑏) ↑m (Base‘𝑎))ℎ = 𝑘)) |
| 40 | 32, 39 | mpbird 257 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ ℎ:(Base‘𝑎)⟶(Base‘𝑏)) → ∃𝑘 ∈ ((Base‘𝑏) ↑m (Base‘𝑎))ℎ = ((𝑎𝐺𝑏)‘𝑘)) |
| 41 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (Hom
‘𝐸) = (Hom
‘𝐸) |
| 42 | 1, 5 | estrcbas 18169 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑈 = (Base‘𝐸)) |
| 43 | 3, 42 | eqtr4id 2796 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 = 𝑈) |
| 44 | 43 | eleq2d 2827 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑎 ∈ 𝐵 ↔ 𝑎 ∈ 𝑈)) |
| 45 | 44 | biimpcd 249 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ 𝐵 → (𝜑 → 𝑎 ∈ 𝑈)) |
| 46 | 45 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝜑 → 𝑎 ∈ 𝑈)) |
| 47 | 46 | impcom 407 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑎 ∈ 𝑈) |
| 48 | 43 | eleq2d 2827 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑏 ∈ 𝐵 ↔ 𝑏 ∈ 𝑈)) |
| 49 | 48 | biimpcd 249 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ 𝐵 → (𝜑 → 𝑏 ∈ 𝑈)) |
| 50 | 49 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝜑 → 𝑏 ∈ 𝑈)) |
| 51 | 50 | impcom 407 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ 𝑈) |
| 52 | 1, 10, 41, 47, 51, 33, 34 | estrchom 18171 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(Hom ‘𝐸)𝑏) = ((Base‘𝑏) ↑m (Base‘𝑎))) |
| 53 | 52 | rexeqdv 3327 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (∃𝑘 ∈ (𝑎(Hom ‘𝐸)𝑏)ℎ = ((𝑎𝐺𝑏)‘𝑘) ↔ ∃𝑘 ∈ ((Base‘𝑏) ↑m (Base‘𝑎))ℎ = ((𝑎𝐺𝑏)‘𝑘))) |
| 54 | 53 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ ℎ:(Base‘𝑎)⟶(Base‘𝑏)) → (∃𝑘 ∈ (𝑎(Hom ‘𝐸)𝑏)ℎ = ((𝑎𝐺𝑏)‘𝑘) ↔ ∃𝑘 ∈ ((Base‘𝑏) ↑m (Base‘𝑎))ℎ = ((𝑎𝐺𝑏)‘𝑘))) |
| 55 | 40, 54 | mpbird 257 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ ℎ:(Base‘𝑎)⟶(Base‘𝑏)) → ∃𝑘 ∈ (𝑎(Hom ‘𝐸)𝑏)ℎ = ((𝑎𝐺𝑏)‘𝑘)) |
| 56 | 55 | ex 412 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (ℎ:(Base‘𝑎)⟶(Base‘𝑏) → ∃𝑘 ∈ (𝑎(Hom ‘𝐸)𝑏)ℎ = ((𝑎𝐺𝑏)‘𝑘))) |
| 57 | 22, 56 | sylbid 240 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (ℎ ∈ ((𝐹‘𝑎)(Hom ‘𝑆)(𝐹‘𝑏)) → ∃𝑘 ∈ (𝑎(Hom ‘𝐸)𝑏)ℎ = ((𝑎𝐺𝑏)‘𝑘))) |
| 58 | 57 | ralrimiv 3145 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ∀ℎ ∈ ((𝐹‘𝑎)(Hom ‘𝑆)(𝐹‘𝑏))∃𝑘 ∈ (𝑎(Hom ‘𝐸)𝑏)ℎ = ((𝑎𝐺𝑏)‘𝑘)) |
| 59 | | dffo3 7122 |
. . . 4
⊢ ((𝑎𝐺𝑏):(𝑎(Hom ‘𝐸)𝑏)–onto→((𝐹‘𝑎)(Hom ‘𝑆)(𝐹‘𝑏)) ↔ ((𝑎𝐺𝑏):(𝑎(Hom ‘𝐸)𝑏)⟶((𝐹‘𝑎)(Hom ‘𝑆)(𝐹‘𝑏)) ∧ ∀ℎ ∈ ((𝐹‘𝑎)(Hom ‘𝑆)(𝐹‘𝑏))∃𝑘 ∈ (𝑎(Hom ‘𝐸)𝑏)ℎ = ((𝑎𝐺𝑏)‘𝑘))) |
| 60 | 9, 58, 59 | sylanbrc 583 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎𝐺𝑏):(𝑎(Hom ‘𝐸)𝑏)–onto→((𝐹‘𝑎)(Hom ‘𝑆)(𝐹‘𝑏))) |
| 61 | 60 | ralrimivva 3202 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎𝐺𝑏):(𝑎(Hom ‘𝐸)𝑏)–onto→((𝐹‘𝑎)(Hom ‘𝑆)(𝐹‘𝑏))) |
| 62 | 3, 11, 41 | isfull2 17958 |
. 2
⊢ (𝐹(𝐸 Full 𝑆)𝐺 ↔ (𝐹(𝐸 Func 𝑆)𝐺 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎𝐺𝑏):(𝑎(Hom ‘𝐸)𝑏)–onto→((𝐹‘𝑎)(Hom ‘𝑆)(𝐹‘𝑏)))) |
| 63 | 8, 61, 62 | sylanbrc 583 |
1
⊢ (𝜑 → 𝐹(𝐸 Full 𝑆)𝐺) |