| Step | Hyp | Ref
| Expression |
| 1 | | f1oi 6886 |
. . . 4
⊢ ( I
↾ ((Base‘𝑌)
↑m (Base‘𝑋))):((Base‘𝑌) ↑m (Base‘𝑋))–1-1-onto→((Base‘𝑌) ↑m (Base‘𝑋)) |
| 2 | | f1of 6848 |
. . . 4
⊢ (( I
↾ ((Base‘𝑌)
↑m (Base‘𝑋))):((Base‘𝑌) ↑m (Base‘𝑋))–1-1-onto→((Base‘𝑌) ↑m (Base‘𝑋)) → ( I ↾
((Base‘𝑌)
↑m (Base‘𝑋))):((Base‘𝑌) ↑m (Base‘𝑋))⟶((Base‘𝑌) ↑m
(Base‘𝑋))) |
| 3 | 1, 2 | mp1i 13 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ( I ↾ ((Base‘𝑌) ↑m
(Base‘𝑋))):((Base‘𝑌) ↑m (Base‘𝑋))⟶((Base‘𝑌) ↑m
(Base‘𝑋))) |
| 4 | | elmapi 8889 |
. . . . 5
⊢ (𝑓 ∈ ((Base‘𝑌) ↑m
(Base‘𝑋)) →
𝑓:(Base‘𝑋)⟶(Base‘𝑌)) |
| 5 | | fvex 6919 |
. . . . . . . . . 10
⊢
(Base‘𝑌)
∈ V |
| 6 | | fvex 6919 |
. . . . . . . . . 10
⊢
(Base‘𝑋)
∈ V |
| 7 | 5, 6 | pm3.2i 470 |
. . . . . . . . 9
⊢
((Base‘𝑌)
∈ V ∧ (Base‘𝑋) ∈ V) |
| 8 | | elmapg 8879 |
. . . . . . . . . 10
⊢
(((Base‘𝑌)
∈ V ∧ (Base‘𝑋) ∈ V) → (𝑓 ∈ ((Base‘𝑌) ↑m (Base‘𝑋)) ↔ 𝑓:(Base‘𝑋)⟶(Base‘𝑌))) |
| 9 | 8 | bicomd 223 |
. . . . . . . . 9
⊢
(((Base‘𝑌)
∈ V ∧ (Base‘𝑋) ∈ V) → (𝑓:(Base‘𝑋)⟶(Base‘𝑌) ↔ 𝑓 ∈ ((Base‘𝑌) ↑m (Base‘𝑋)))) |
| 10 | 7, 9 | mp1i 13 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑓:(Base‘𝑋)⟶(Base‘𝑌) ↔ 𝑓 ∈ ((Base‘𝑌) ↑m (Base‘𝑋)))) |
| 11 | 10 | biimpa 476 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑓:(Base‘𝑋)⟶(Base‘𝑌)) → 𝑓 ∈ ((Base‘𝑌) ↑m (Base‘𝑋))) |
| 12 | | funcestrcsetc.e |
. . . . . . . . . . 11
⊢ 𝐸 = (ExtStrCat‘𝑈) |
| 13 | | funcestrcsetc.s |
. . . . . . . . . . 11
⊢ 𝑆 = (SetCat‘𝑈) |
| 14 | | funcestrcsetc.b |
. . . . . . . . . . 11
⊢ 𝐵 = (Base‘𝐸) |
| 15 | | funcestrcsetc.c |
. . . . . . . . . . 11
⊢ 𝐶 = (Base‘𝑆) |
| 16 | | funcestrcsetc.u |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ WUni) |
| 17 | | funcestrcsetc.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) |
| 18 | 12, 13, 14, 15, 16, 17 | funcestrcsetclem1 18185 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑌 ∈ 𝐵) → (𝐹‘𝑌) = (Base‘𝑌)) |
| 19 | 18 | adantrl 716 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑌) = (Base‘𝑌)) |
| 20 | 12, 13, 14, 15, 16, 17 | funcestrcsetclem1 18185 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) = (Base‘𝑋)) |
| 21 | 20 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑋) = (Base‘𝑋)) |
| 22 | 19, 21 | oveq12d 7449 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐹‘𝑌) ↑m (𝐹‘𝑋)) = ((Base‘𝑌) ↑m (Base‘𝑋))) |
| 23 | 22 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑓:(Base‘𝑋)⟶(Base‘𝑌)) → ((𝐹‘𝑌) ↑m (𝐹‘𝑋)) = ((Base‘𝑌) ↑m (Base‘𝑋))) |
| 24 | 11, 23 | eleqtrrd 2844 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑓:(Base‘𝑋)⟶(Base‘𝑌)) → 𝑓 ∈ ((𝐹‘𝑌) ↑m (𝐹‘𝑋))) |
| 25 | 24 | ex 412 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑓:(Base‘𝑋)⟶(Base‘𝑌) → 𝑓 ∈ ((𝐹‘𝑌) ↑m (𝐹‘𝑋)))) |
| 26 | 4, 25 | syl5 34 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑓 ∈ ((Base‘𝑌) ↑m (Base‘𝑋)) → 𝑓 ∈ ((𝐹‘𝑌) ↑m (𝐹‘𝑋)))) |
| 27 | 26 | ssrdv 3989 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((Base‘𝑌) ↑m (Base‘𝑋)) ⊆ ((𝐹‘𝑌) ↑m (𝐹‘𝑋))) |
| 28 | 3, 27 | fssd 6753 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ( I ↾ ((Base‘𝑌) ↑m
(Base‘𝑋))):((Base‘𝑌) ↑m (Base‘𝑋))⟶((𝐹‘𝑌) ↑m (𝐹‘𝑋))) |
| 29 | | funcestrcsetc.g |
. . . 4
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))) |
| 30 | | eqid 2737 |
. . . 4
⊢
(Base‘𝑋) =
(Base‘𝑋) |
| 31 | | eqid 2737 |
. . . 4
⊢
(Base‘𝑌) =
(Base‘𝑌) |
| 32 | 12, 13, 14, 15, 16, 17, 29, 30, 31 | funcestrcsetclem5 18189 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐺𝑌) = ( I ↾ ((Base‘𝑌) ↑m
(Base‘𝑋)))) |
| 33 | 16 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑈 ∈ WUni) |
| 34 | | eqid 2737 |
. . . 4
⊢ (Hom
‘𝐸) = (Hom
‘𝐸) |
| 35 | 12, 16 | estrcbas 18169 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 = (Base‘𝐸)) |
| 36 | 14, 35 | eqtr4id 2796 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 = 𝑈) |
| 37 | 36 | eleq2d 2827 |
. . . . . . 7
⊢ (𝜑 → (𝑋 ∈ 𝐵 ↔ 𝑋 ∈ 𝑈)) |
| 38 | 37 | biimpcd 249 |
. . . . . 6
⊢ (𝑋 ∈ 𝐵 → (𝜑 → 𝑋 ∈ 𝑈)) |
| 39 | 38 | adantr 480 |
. . . . 5
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝜑 → 𝑋 ∈ 𝑈)) |
| 40 | 39 | impcom 407 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋 ∈ 𝑈) |
| 41 | 36 | eleq2d 2827 |
. . . . . . 7
⊢ (𝜑 → (𝑌 ∈ 𝐵 ↔ 𝑌 ∈ 𝑈)) |
| 42 | 41 | biimpd 229 |
. . . . . 6
⊢ (𝜑 → (𝑌 ∈ 𝐵 → 𝑌 ∈ 𝑈)) |
| 43 | 42 | adantld 490 |
. . . . 5
⊢ (𝜑 → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝑈)) |
| 44 | 43 | imp 406 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌 ∈ 𝑈) |
| 45 | 12, 33, 34, 40, 44, 30, 31 | estrchom 18171 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(Hom ‘𝐸)𝑌) = ((Base‘𝑌) ↑m (Base‘𝑋))) |
| 46 | | eqid 2737 |
. . . 4
⊢ (Hom
‘𝑆) = (Hom
‘𝑆) |
| 47 | 12, 13, 14, 15, 16, 17 | funcestrcsetclem2 18186 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ 𝑈) |
| 48 | 47 | adantrr 717 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑋) ∈ 𝑈) |
| 49 | 12, 13, 14, 15, 16, 17 | funcestrcsetclem2 18186 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 ∈ 𝐵) → (𝐹‘𝑌) ∈ 𝑈) |
| 50 | 49 | adantrl 716 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑌) ∈ 𝑈) |
| 51 | 13, 33, 46, 48, 50 | setchom 18125 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐹‘𝑋)(Hom ‘𝑆)(𝐹‘𝑌)) = ((𝐹‘𝑌) ↑m (𝐹‘𝑋))) |
| 52 | 32, 45, 51 | feq123d 6725 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑋𝐺𝑌):(𝑋(Hom ‘𝐸)𝑌)⟶((𝐹‘𝑋)(Hom ‘𝑆)(𝐹‘𝑌)) ↔ ( I ↾ ((Base‘𝑌) ↑m
(Base‘𝑋))):((Base‘𝑌) ↑m (Base‘𝑋))⟶((𝐹‘𝑌) ↑m (𝐹‘𝑋)))) |
| 53 | 28, 52 | mpbird 257 |
1
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐺𝑌):(𝑋(Hom ‘𝐸)𝑌)⟶((𝐹‘𝑋)(Hom ‘𝑆)(𝐹‘𝑌))) |