Proof of Theorem funcsetcestrclem9
| Step | Hyp | Ref
| Expression |
| 1 | | funcsetcestrc.s |
. . . . . 6
⊢ 𝑆 = (SetCat‘𝑈) |
| 2 | | funcsetcestrc.u |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ WUni) |
| 3 | 2 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → 𝑈 ∈ WUni) |
| 4 | | eqid 2737 |
. . . . . 6
⊢ (Hom
‘𝑆) = (Hom
‘𝑆) |
| 5 | | funcsetcestrc.c |
. . . . . . . . . . 11
⊢ 𝐶 = (Base‘𝑆) |
| 6 | 1, 2 | setcbas 18123 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 = (Base‘𝑆)) |
| 7 | 5, 6 | eqtr4id 2796 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 = 𝑈) |
| 8 | 7 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 ∈ 𝐶 ↔ 𝑋 ∈ 𝑈)) |
| 9 | 8 | biimpcd 249 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐶 → (𝜑 → 𝑋 ∈ 𝑈)) |
| 10 | 9 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶) → (𝜑 → 𝑋 ∈ 𝑈)) |
| 11 | 10 | impcom 407 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → 𝑋 ∈ 𝑈) |
| 12 | 7 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌 ∈ 𝐶 ↔ 𝑌 ∈ 𝑈)) |
| 13 | 12 | biimpcd 249 |
. . . . . . . 8
⊢ (𝑌 ∈ 𝐶 → (𝜑 → 𝑌 ∈ 𝑈)) |
| 14 | 13 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶) → (𝜑 → 𝑌 ∈ 𝑈)) |
| 15 | 14 | impcom 407 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → 𝑌 ∈ 𝑈) |
| 16 | 1, 3, 4, 11, 15 | setchom 18125 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → (𝑋(Hom ‘𝑆)𝑌) = (𝑌 ↑m 𝑋)) |
| 17 | 16 | eleq2d 2827 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → (𝐻 ∈ (𝑋(Hom ‘𝑆)𝑌) ↔ 𝐻 ∈ (𝑌 ↑m 𝑋))) |
| 18 | 7 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝜑 → (𝑍 ∈ 𝐶 ↔ 𝑍 ∈ 𝑈)) |
| 19 | 18 | biimpcd 249 |
. . . . . . . 8
⊢ (𝑍 ∈ 𝐶 → (𝜑 → 𝑍 ∈ 𝑈)) |
| 20 | 19 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶) → (𝜑 → 𝑍 ∈ 𝑈)) |
| 21 | 20 | impcom 407 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → 𝑍 ∈ 𝑈) |
| 22 | 1, 3, 4, 15, 21 | setchom 18125 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → (𝑌(Hom ‘𝑆)𝑍) = (𝑍 ↑m 𝑌)) |
| 23 | 22 | eleq2d 2827 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → (𝐾 ∈ (𝑌(Hom ‘𝑆)𝑍) ↔ 𝐾 ∈ (𝑍 ↑m 𝑌))) |
| 24 | 17, 23 | anbi12d 632 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → ((𝐻 ∈ (𝑋(Hom ‘𝑆)𝑌) ∧ 𝐾 ∈ (𝑌(Hom ‘𝑆)𝑍)) ↔ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌)))) |
| 25 | | elmapi 8889 |
. . . . . . . . 9
⊢ (𝐾 ∈ (𝑍 ↑m 𝑌) → 𝐾:𝑌⟶𝑍) |
| 26 | | elmapi 8889 |
. . . . . . . . 9
⊢ (𝐻 ∈ (𝑌 ↑m 𝑋) → 𝐻:𝑋⟶𝑌) |
| 27 | | fco 6760 |
. . . . . . . . 9
⊢ ((𝐾:𝑌⟶𝑍 ∧ 𝐻:𝑋⟶𝑌) → (𝐾 ∘ 𝐻):𝑋⟶𝑍) |
| 28 | 25, 26, 27 | syl2anr 597 |
. . . . . . . 8
⊢ ((𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌)) → (𝐾 ∘ 𝐻):𝑋⟶𝑍) |
| 29 | 28 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → (𝐾 ∘ 𝐻):𝑋⟶𝑍) |
| 30 | | elmapg 8879 |
. . . . . . . . . 10
⊢ ((𝑍 ∈ 𝐶 ∧ 𝑋 ∈ 𝐶) → ((𝐾 ∘ 𝐻) ∈ (𝑍 ↑m 𝑋) ↔ (𝐾 ∘ 𝐻):𝑋⟶𝑍)) |
| 31 | 30 | ancoms 458 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶) → ((𝐾 ∘ 𝐻) ∈ (𝑍 ↑m 𝑋) ↔ (𝐾 ∘ 𝐻):𝑋⟶𝑍)) |
| 32 | 31 | 3adant2 1132 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶) → ((𝐾 ∘ 𝐻) ∈ (𝑍 ↑m 𝑋) ↔ (𝐾 ∘ 𝐻):𝑋⟶𝑍)) |
| 33 | 32 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → ((𝐾 ∘ 𝐻) ∈ (𝑍 ↑m 𝑋) ↔ (𝐾 ∘ 𝐻):𝑋⟶𝑍)) |
| 34 | 29, 33 | mpbird 257 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → (𝐾 ∘ 𝐻) ∈ (𝑍 ↑m 𝑋)) |
| 35 | | fvresi 7193 |
. . . . . 6
⊢ ((𝐾 ∘ 𝐻) ∈ (𝑍 ↑m 𝑋) → (( I ↾ (𝑍 ↑m 𝑋))‘(𝐾 ∘ 𝐻)) = (𝐾 ∘ 𝐻)) |
| 36 | 34, 35 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → (( I ↾ (𝑍 ↑m 𝑋))‘(𝐾 ∘ 𝐻)) = (𝐾 ∘ 𝐻)) |
| 37 | | funcsetcestrc.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) |
| 38 | | funcsetcestrc.o |
. . . . . . . . 9
⊢ (𝜑 → ω ∈ 𝑈) |
| 39 | | funcsetcestrc.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥)))) |
| 40 | 1, 5, 37, 2, 38, 39 | funcsetcestrclem5 18204 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → (𝑋𝐺𝑍) = ( I ↾ (𝑍 ↑m 𝑋))) |
| 41 | 40 | 3adantr2 1171 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → (𝑋𝐺𝑍) = ( I ↾ (𝑍 ↑m 𝑋))) |
| 42 | 41 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → (𝑋𝐺𝑍) = ( I ↾ (𝑍 ↑m 𝑋))) |
| 43 | 3 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → 𝑈 ∈ WUni) |
| 44 | | eqid 2737 |
. . . . . . 7
⊢
(comp‘𝑆) =
(comp‘𝑆) |
| 45 | 11 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → 𝑋 ∈ 𝑈) |
| 46 | 15 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → 𝑌 ∈ 𝑈) |
| 47 | 21 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → 𝑍 ∈ 𝑈) |
| 48 | 26 | ad2antrl 728 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → 𝐻:𝑋⟶𝑌) |
| 49 | 25 | ad2antll 729 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → 𝐾:𝑌⟶𝑍) |
| 50 | 1, 43, 44, 45, 46, 47, 48, 49 | setcco 18128 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → (𝐾(〈𝑋, 𝑌〉(comp‘𝑆)𝑍)𝐻) = (𝐾 ∘ 𝐻)) |
| 51 | 42, 50 | fveq12d 6913 |
. . . . 5
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → ((𝑋𝐺𝑍)‘(𝐾(〈𝑋, 𝑌〉(comp‘𝑆)𝑍)𝐻)) = (( I ↾ (𝑍 ↑m 𝑋))‘(𝐾 ∘ 𝐻))) |
| 52 | | funcsetcestrc.e |
. . . . . . 7
⊢ 𝐸 = (ExtStrCat‘𝑈) |
| 53 | | eqid 2737 |
. . . . . . 7
⊢
(comp‘𝐸) =
(comp‘𝐸) |
| 54 | 1, 5, 37, 2, 38 | funcsetcestrclem2 18200 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐹‘𝑋) ∈ 𝑈) |
| 55 | 54 | 3ad2antr1 1189 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → (𝐹‘𝑋) ∈ 𝑈) |
| 56 | 55 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → (𝐹‘𝑋) ∈ 𝑈) |
| 57 | 1, 5, 37, 2, 38 | funcsetcestrclem2 18200 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑌 ∈ 𝐶) → (𝐹‘𝑌) ∈ 𝑈) |
| 58 | 57 | 3ad2antr2 1190 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → (𝐹‘𝑌) ∈ 𝑈) |
| 59 | 58 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → (𝐹‘𝑌) ∈ 𝑈) |
| 60 | 1, 5, 37, 2, 38 | funcsetcestrclem2 18200 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑍 ∈ 𝐶) → (𝐹‘𝑍) ∈ 𝑈) |
| 61 | 60 | 3ad2antr3 1191 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → (𝐹‘𝑍) ∈ 𝑈) |
| 62 | 61 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → (𝐹‘𝑍) ∈ 𝑈) |
| 63 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘(𝐹‘𝑋)) = (Base‘(𝐹‘𝑋)) |
| 64 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘(𝐹‘𝑌)) = (Base‘(𝐹‘𝑌)) |
| 65 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘(𝐹‘𝑍)) = (Base‘(𝐹‘𝑍)) |
| 66 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → 𝜑) |
| 67 | | 3simpa 1149 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶) → (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) |
| 68 | 67 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) |
| 69 | | simprl 771 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → 𝐻 ∈ (𝑌 ↑m 𝑋)) |
| 70 | 1, 5, 37, 2, 38, 39 | funcsetcestrclem6 18205 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝐻 ∈ (𝑌 ↑m 𝑋)) → ((𝑋𝐺𝑌)‘𝐻) = 𝐻) |
| 71 | 66, 68, 69, 70 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → ((𝑋𝐺𝑌)‘𝐻) = 𝐻) |
| 72 | 1, 5, 37 | funcsetcestrclem1 18199 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐹‘𝑋) = {〈(Base‘ndx), 𝑋〉}) |
| 73 | 72 | 3ad2antr1 1189 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → (𝐹‘𝑋) = {〈(Base‘ndx), 𝑋〉}) |
| 74 | 73 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → (Base‘(𝐹‘𝑋)) = (Base‘{〈(Base‘ndx),
𝑋〉})) |
| 75 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
{〈(Base‘ndx), 𝑋〉} = {〈(Base‘ndx), 𝑋〉} |
| 76 | 75 | 1strbas 17263 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ 𝐶 → 𝑋 = (Base‘{〈(Base‘ndx),
𝑋〉})) |
| 77 | 76 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ 𝐶 → (Base‘{〈(Base‘ndx),
𝑋〉}) = 𝑋) |
| 78 | 77 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶) →
(Base‘{〈(Base‘ndx), 𝑋〉}) = 𝑋) |
| 79 | 78 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) →
(Base‘{〈(Base‘ndx), 𝑋〉}) = 𝑋) |
| 80 | 74, 79 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → (Base‘(𝐹‘𝑋)) = 𝑋) |
| 81 | 80 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → (Base‘(𝐹‘𝑋)) = 𝑋) |
| 82 | 1, 5, 37 | funcsetcestrclem1 18199 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ∈ 𝐶) → (𝐹‘𝑌) = {〈(Base‘ndx), 𝑌〉}) |
| 83 | 82 | 3ad2antr2 1190 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → (𝐹‘𝑌) = {〈(Base‘ndx), 𝑌〉}) |
| 84 | 83 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → (Base‘(𝐹‘𝑌)) = (Base‘{〈(Base‘ndx),
𝑌〉})) |
| 85 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
{〈(Base‘ndx), 𝑌〉} = {〈(Base‘ndx), 𝑌〉} |
| 86 | 85 | 1strbas 17263 |
. . . . . . . . . . . . . 14
⊢ (𝑌 ∈ 𝐶 → 𝑌 = (Base‘{〈(Base‘ndx),
𝑌〉})) |
| 87 | 86 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ 𝐶 → (Base‘{〈(Base‘ndx),
𝑌〉}) = 𝑌) |
| 88 | 87 | 3ad2ant2 1135 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶) →
(Base‘{〈(Base‘ndx), 𝑌〉}) = 𝑌) |
| 89 | 88 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) →
(Base‘{〈(Base‘ndx), 𝑌〉}) = 𝑌) |
| 90 | 84, 89 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → (Base‘(𝐹‘𝑌)) = 𝑌) |
| 91 | 90 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → (Base‘(𝐹‘𝑌)) = 𝑌) |
| 92 | 71, 81, 91 | feq123d 6725 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → (((𝑋𝐺𝑌)‘𝐻):(Base‘(𝐹‘𝑋))⟶(Base‘(𝐹‘𝑌)) ↔ 𝐻:𝑋⟶𝑌)) |
| 93 | 48, 92 | mpbird 257 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → ((𝑋𝐺𝑌)‘𝐻):(Base‘(𝐹‘𝑋))⟶(Base‘(𝐹‘𝑌))) |
| 94 | | 3simpc 1151 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶) → (𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) |
| 95 | 94 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → (𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) |
| 96 | | simprr 773 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → 𝐾 ∈ (𝑍 ↑m 𝑌)) |
| 97 | 1, 5, 37, 2, 38, 39 | funcsetcestrclem6 18205 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌)) → ((𝑌𝐺𝑍)‘𝐾) = 𝐾) |
| 98 | 66, 95, 96, 97 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → ((𝑌𝐺𝑍)‘𝐾) = 𝐾) |
| 99 | 1, 5, 37 | funcsetcestrclem1 18199 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑍 ∈ 𝐶) → (𝐹‘𝑍) = {〈(Base‘ndx), 𝑍〉}) |
| 100 | 99 | 3ad2antr3 1191 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → (𝐹‘𝑍) = {〈(Base‘ndx), 𝑍〉}) |
| 101 | 100 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → (Base‘(𝐹‘𝑍)) = (Base‘{〈(Base‘ndx),
𝑍〉})) |
| 102 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
{〈(Base‘ndx), 𝑍〉} = {〈(Base‘ndx), 𝑍〉} |
| 103 | 102 | 1strbas 17263 |
. . . . . . . . . . . . . 14
⊢ (𝑍 ∈ 𝐶 → 𝑍 = (Base‘{〈(Base‘ndx),
𝑍〉})) |
| 104 | 103 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢ (𝑍 ∈ 𝐶 → (Base‘{〈(Base‘ndx),
𝑍〉}) = 𝑍) |
| 105 | 104 | 3ad2ant3 1136 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶) →
(Base‘{〈(Base‘ndx), 𝑍〉}) = 𝑍) |
| 106 | 105 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) →
(Base‘{〈(Base‘ndx), 𝑍〉}) = 𝑍) |
| 107 | 101, 106 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → (Base‘(𝐹‘𝑍)) = 𝑍) |
| 108 | 107 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → (Base‘(𝐹‘𝑍)) = 𝑍) |
| 109 | 98, 91, 108 | feq123d 6725 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → (((𝑌𝐺𝑍)‘𝐾):(Base‘(𝐹‘𝑌))⟶(Base‘(𝐹‘𝑍)) ↔ 𝐾:𝑌⟶𝑍)) |
| 110 | 49, 109 | mpbird 257 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → ((𝑌𝐺𝑍)‘𝐾):(Base‘(𝐹‘𝑌))⟶(Base‘(𝐹‘𝑍))) |
| 111 | 52, 43, 53, 56, 59, 62, 63, 64, 65, 93, 110 | estrcco 18174 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → (((𝑌𝐺𝑍)‘𝐾)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉(comp‘𝐸)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐻)) = (((𝑌𝐺𝑍)‘𝐾) ∘ ((𝑋𝐺𝑌)‘𝐻))) |
| 112 | 98, 71 | coeq12d 5875 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → (((𝑌𝐺𝑍)‘𝐾) ∘ ((𝑋𝐺𝑌)‘𝐻)) = (𝐾 ∘ 𝐻)) |
| 113 | 111, 112 | eqtrd 2777 |
. . . . 5
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → (((𝑌𝐺𝑍)‘𝐾)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉(comp‘𝐸)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐻)) = (𝐾 ∘ 𝐻)) |
| 114 | 36, 51, 113 | 3eqtr4d 2787 |
. . . 4
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) ∧ (𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌))) → ((𝑋𝐺𝑍)‘(𝐾(〈𝑋, 𝑌〉(comp‘𝑆)𝑍)𝐻)) = (((𝑌𝐺𝑍)‘𝐾)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉(comp‘𝐸)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐻))) |
| 115 | 114 | ex 412 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → ((𝐻 ∈ (𝑌 ↑m 𝑋) ∧ 𝐾 ∈ (𝑍 ↑m 𝑌)) → ((𝑋𝐺𝑍)‘(𝐾(〈𝑋, 𝑌〉(comp‘𝑆)𝑍)𝐻)) = (((𝑌𝐺𝑍)‘𝐾)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉(comp‘𝐸)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐻)))) |
| 116 | 24, 115 | sylbid 240 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶)) → ((𝐻 ∈ (𝑋(Hom ‘𝑆)𝑌) ∧ 𝐾 ∈ (𝑌(Hom ‘𝑆)𝑍)) → ((𝑋𝐺𝑍)‘(𝐾(〈𝑋, 𝑌〉(comp‘𝑆)𝑍)𝐻)) = (((𝑌𝐺𝑍)‘𝐾)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉(comp‘𝐸)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐻)))) |
| 117 | 116 | 3impia 1118 |
1
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶) ∧ (𝐻 ∈ (𝑋(Hom ‘𝑆)𝑌) ∧ 𝐾 ∈ (𝑌(Hom ‘𝑆)𝑍))) → ((𝑋𝐺𝑍)‘(𝐾(〈𝑋, 𝑌〉(comp‘𝑆)𝑍)𝐻)) = (((𝑌𝐺𝑍)‘𝐾)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉(comp‘𝐸)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐻))) |