Step | Hyp | Ref
| Expression |
1 | | f1oi 6719 |
. . . 4
⊢ ( I
↾ (𝑌
↑m 𝑋)):(𝑌 ↑m 𝑋)–1-1-onto→(𝑌 ↑m 𝑋) |
2 | | f1of 6682 |
. . . 4
⊢ (( I
↾ (𝑌
↑m 𝑋)):(𝑌 ↑m 𝑋)–1-1-onto→(𝑌 ↑m 𝑋) → ( I ↾ (𝑌 ↑m 𝑋)):(𝑌 ↑m 𝑋)⟶(𝑌 ↑m 𝑋)) |
3 | 1, 2 | mp1i 13 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → ( I ↾ (𝑌 ↑m 𝑋)):(𝑌 ↑m 𝑋)⟶(𝑌 ↑m 𝑋)) |
4 | | elmapi 8553 |
. . . . 5
⊢ (𝑓 ∈ (𝑌 ↑m 𝑋) → 𝑓:𝑋⟶𝑌) |
5 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) |
6 | 5 | ancomd 465 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑌 ∈ 𝐶 ∧ 𝑋 ∈ 𝐶)) |
7 | | elmapg 8544 |
. . . . . . . . 9
⊢ ((𝑌 ∈ 𝐶 ∧ 𝑋 ∈ 𝐶) → (𝑓 ∈ (𝑌 ↑m 𝑋) ↔ 𝑓:𝑋⟶𝑌)) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑓 ∈ (𝑌 ↑m 𝑋) ↔ 𝑓:𝑋⟶𝑌)) |
9 | 8 | biimpar 481 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) ∧ 𝑓:𝑋⟶𝑌) → 𝑓 ∈ (𝑌 ↑m 𝑋)) |
10 | | funcsetcestrc.s |
. . . . . . . . . . . . 13
⊢ 𝑆 = (SetCat‘𝑈) |
11 | | funcsetcestrc.c |
. . . . . . . . . . . . 13
⊢ 𝐶 = (Base‘𝑆) |
12 | | funcsetcestrc.f |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) |
13 | 10, 11, 12 | funcsetcestrclem1 17693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ∈ 𝐶) → (𝐹‘𝑌) = {〈(Base‘ndx), 𝑌〉}) |
14 | 13 | fveq2d 6742 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑌 ∈ 𝐶) → (Base‘(𝐹‘𝑌)) = (Base‘{〈(Base‘ndx),
𝑌〉})) |
15 | | eqid 2739 |
. . . . . . . . . . . . . 14
⊢
{〈(Base‘ndx), 𝑌〉} = {〈(Base‘ndx), 𝑌〉} |
16 | 15 | 1strbas 16807 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ 𝐶 → 𝑌 = (Base‘{〈(Base‘ndx),
𝑌〉})) |
17 | 16 | eqcomd 2745 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ 𝐶 → (Base‘{〈(Base‘ndx),
𝑌〉}) = 𝑌) |
18 | 17 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑌 ∈ 𝐶) →
(Base‘{〈(Base‘ndx), 𝑌〉}) = 𝑌) |
19 | 14, 18 | eqtrd 2779 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑌 ∈ 𝐶) → (Base‘(𝐹‘𝑌)) = 𝑌) |
20 | 19 | adantrl 716 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (Base‘(𝐹‘𝑌)) = 𝑌) |
21 | 10, 11, 12 | funcsetcestrclem1 17693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐹‘𝑋) = {〈(Base‘ndx), 𝑋〉}) |
22 | 21 | fveq2d 6742 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (Base‘(𝐹‘𝑋)) = (Base‘{〈(Base‘ndx),
𝑋〉})) |
23 | | eqid 2739 |
. . . . . . . . . . . . 13
⊢
{〈(Base‘ndx), 𝑋〉} = {〈(Base‘ndx), 𝑋〉} |
24 | 23 | 1strbas 16807 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝐶 → 𝑋 = (Base‘{〈(Base‘ndx),
𝑋〉})) |
25 | 24 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 𝑋 = (Base‘{〈(Base‘ndx),
𝑋〉})) |
26 | 22, 25 | eqtr4d 2782 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (Base‘(𝐹‘𝑋)) = 𝑋) |
27 | 26 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (Base‘(𝐹‘𝑋)) = 𝑋) |
28 | 20, 27 | oveq12d 7252 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → ((Base‘(𝐹‘𝑌)) ↑m (Base‘(𝐹‘𝑋))) = (𝑌 ↑m 𝑋)) |
29 | 28 | adantr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) ∧ 𝑓:𝑋⟶𝑌) → ((Base‘(𝐹‘𝑌)) ↑m (Base‘(𝐹‘𝑋))) = (𝑌 ↑m 𝑋)) |
30 | 9, 29 | eleqtrrd 2843 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) ∧ 𝑓:𝑋⟶𝑌) → 𝑓 ∈ ((Base‘(𝐹‘𝑌)) ↑m (Base‘(𝐹‘𝑋)))) |
31 | 30 | ex 416 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑓:𝑋⟶𝑌 → 𝑓 ∈ ((Base‘(𝐹‘𝑌)) ↑m (Base‘(𝐹‘𝑋))))) |
32 | 4, 31 | syl5 34 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑓 ∈ (𝑌 ↑m 𝑋) → 𝑓 ∈ ((Base‘(𝐹‘𝑌)) ↑m (Base‘(𝐹‘𝑋))))) |
33 | 32 | ssrdv 3923 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑌 ↑m 𝑋) ⊆ ((Base‘(𝐹‘𝑌)) ↑m (Base‘(𝐹‘𝑋)))) |
34 | 3, 33 | fssd 6584 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → ( I ↾ (𝑌 ↑m 𝑋)):(𝑌 ↑m 𝑋)⟶((Base‘(𝐹‘𝑌)) ↑m (Base‘(𝐹‘𝑋)))) |
35 | | funcsetcestrc.u |
. . . 4
⊢ (𝜑 → 𝑈 ∈ WUni) |
36 | | funcsetcestrc.o |
. . . 4
⊢ (𝜑 → ω ∈ 𝑈) |
37 | | funcsetcestrc.g |
. . . 4
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥)))) |
38 | 10, 11, 12, 35, 36, 37 | funcsetcestrclem5 17698 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋𝐺𝑌) = ( I ↾ (𝑌 ↑m 𝑋))) |
39 | 35 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → 𝑈 ∈ WUni) |
40 | | eqid 2739 |
. . . 4
⊢ (Hom
‘𝑆) = (Hom
‘𝑆) |
41 | 10, 35 | setcbas 17616 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 = (Base‘𝑆)) |
42 | 11, 41 | eqtr4id 2799 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 = 𝑈) |
43 | 42 | eleq2d 2825 |
. . . . . . 7
⊢ (𝜑 → (𝑋 ∈ 𝐶 ↔ 𝑋 ∈ 𝑈)) |
44 | 43 | biimpd 232 |
. . . . . 6
⊢ (𝜑 → (𝑋 ∈ 𝐶 → 𝑋 ∈ 𝑈)) |
45 | 44 | adantrd 495 |
. . . . 5
⊢ (𝜑 → ((𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) → 𝑋 ∈ 𝑈)) |
46 | 45 | imp 410 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → 𝑋 ∈ 𝑈) |
47 | 42 | eleq2d 2825 |
. . . . . . 7
⊢ (𝜑 → (𝑌 ∈ 𝐶 ↔ 𝑌 ∈ 𝑈)) |
48 | 47 | biimpd 232 |
. . . . . 6
⊢ (𝜑 → (𝑌 ∈ 𝐶 → 𝑌 ∈ 𝑈)) |
49 | 48 | adantld 494 |
. . . . 5
⊢ (𝜑 → ((𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) → 𝑌 ∈ 𝑈)) |
50 | 49 | imp 410 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → 𝑌 ∈ 𝑈) |
51 | 10, 39, 40, 46, 50 | setchom 17618 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋(Hom ‘𝑆)𝑌) = (𝑌 ↑m 𝑋)) |
52 | | funcsetcestrc.e |
. . . 4
⊢ 𝐸 = (ExtStrCat‘𝑈) |
53 | | eqid 2739 |
. . . 4
⊢ (Hom
‘𝐸) = (Hom
‘𝐸) |
54 | 10, 11, 12, 35, 36 | funcsetcestrclem2 17694 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐹‘𝑋) ∈ 𝑈) |
55 | 54 | adantrr 717 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝐹‘𝑋) ∈ 𝑈) |
56 | 10, 11, 12, 35, 36 | funcsetcestrclem2 17694 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 ∈ 𝐶) → (𝐹‘𝑌) ∈ 𝑈) |
57 | 56 | adantrl 716 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝐹‘𝑌) ∈ 𝑈) |
58 | | eqid 2739 |
. . . 4
⊢
(Base‘(𝐹‘𝑋)) = (Base‘(𝐹‘𝑋)) |
59 | | eqid 2739 |
. . . 4
⊢
(Base‘(𝐹‘𝑌)) = (Base‘(𝐹‘𝑌)) |
60 | 52, 39, 53, 55, 57, 58, 59 | estrchom 17666 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → ((𝐹‘𝑋)(Hom ‘𝐸)(𝐹‘𝑌)) = ((Base‘(𝐹‘𝑌)) ↑m (Base‘(𝐹‘𝑋)))) |
61 | 38, 51, 60 | feq123d 6555 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → ((𝑋𝐺𝑌):(𝑋(Hom ‘𝑆)𝑌)⟶((𝐹‘𝑋)(Hom ‘𝐸)(𝐹‘𝑌)) ↔ ( I ↾ (𝑌 ↑m 𝑋)):(𝑌 ↑m 𝑋)⟶((Base‘(𝐹‘𝑌)) ↑m (Base‘(𝐹‘𝑋))))) |
62 | 34, 61 | mpbird 260 |
1
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋𝐺𝑌):(𝑋(Hom ‘𝑆)𝑌)⟶((𝐹‘𝑋)(Hom ‘𝐸)(𝐹‘𝑌))) |