Step | Hyp | Ref
| Expression |
1 | | ffn 6045 |
. . . . 5
⊢ (𝐹:𝐴⟶Comp → 𝐹 Fn 𝐴) |
2 | | fnresdm 6000 |
. . . . 5
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝐹:𝐴⟶Comp → (𝐹 ↾ 𝐴) = 𝐹) |
4 | 3 | adantl 482 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (𝐹 ↾ 𝐴) = 𝐹) |
5 | 4 | fveq2d 6195 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ 𝐴)) = (∏t‘𝐹)) |
6 | | ssid 3624 |
. . . 4
⊢ 𝐴 ⊆ 𝐴 |
7 | | sseq1 3626 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝑥 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴)) |
8 | | reseq2 5391 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → (𝐹 ↾ 𝑥) = (𝐹 ↾ ∅)) |
9 | | res0 5400 |
. . . . . . . . . 10
⊢ (𝐹 ↾ ∅) =
∅ |
10 | 8, 9 | syl6eq 2672 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (𝐹 ↾ 𝑥) = ∅) |
11 | 10 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑥 = ∅ →
(∏t‘(𝐹 ↾ 𝑥)) =
(∏t‘∅)) |
12 | 11 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑥 = ∅ →
((∏t‘(𝐹 ↾ 𝑥)) ∈ Comp ↔
(∏t‘∅) ∈ Comp)) |
13 | 12 | imbi2d 330 |
. . . . . 6
⊢ (𝑥 = ∅ → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ 𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘∅) ∈ Comp))) |
14 | 7, 13 | imbi12d 334 |
. . . . 5
⊢ (𝑥 = ∅ → ((𝑥 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ 𝑥)) ∈ Comp)) ↔ (∅ ⊆
𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘∅) ∈ Comp)))) |
15 | | sseq1 3626 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴)) |
16 | | reseq2 5391 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝐹 ↾ 𝑥) = (𝐹 ↾ 𝑦)) |
17 | 16 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (∏t‘(𝐹 ↾ 𝑥)) = (∏t‘(𝐹 ↾ 𝑦))) |
18 | 17 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((∏t‘(𝐹 ↾ 𝑥)) ∈ Comp ↔
(∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)) |
19 | 18 | imbi2d 330 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ 𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ 𝑦)) ∈ Comp))) |
20 | 15, 19 | imbi12d 334 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑥 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ 𝑥)) ∈ Comp)) ↔ (𝑦 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)))) |
21 | | sseq1 3626 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑥 ⊆ 𝐴 ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) |
22 | | reseq2 5391 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐹 ↾ 𝑥) = (𝐹 ↾ (𝑦 ∪ {𝑧}))) |
23 | 22 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∏t‘(𝐹 ↾ 𝑥)) = (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧})))) |
24 | 23 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((∏t‘(𝐹 ↾ 𝑥)) ∈ Comp ↔
(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)) |
25 | 24 | imbi2d 330 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ 𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))) |
26 | 21, 25 | imbi12d 334 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑥 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ 𝑥)) ∈ Comp)) ↔ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)))) |
27 | | sseq1 3626 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴)) |
28 | | reseq2 5391 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (𝐹 ↾ 𝑥) = (𝐹 ↾ 𝐴)) |
29 | 28 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (∏t‘(𝐹 ↾ 𝑥)) = (∏t‘(𝐹 ↾ 𝐴))) |
30 | 29 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((∏t‘(𝐹 ↾ 𝑥)) ∈ Comp ↔
(∏t‘(𝐹 ↾ 𝐴)) ∈ Comp)) |
31 | 30 | imbi2d 330 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ 𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ 𝐴)) ∈ Comp))) |
32 | 27, 31 | imbi12d 334 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((𝑥 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ 𝑥)) ∈ Comp)) ↔ (𝐴 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ 𝐴)) ∈ Comp)))) |
33 | | 0ex 4790 |
. . . . . . . . 9
⊢ ∅
∈ V |
34 | | f0 6086 |
. . . . . . . . 9
⊢
∅:∅⟶Top |
35 | | pttop 21385 |
. . . . . . . . 9
⊢ ((∅
∈ V ∧ ∅:∅⟶Top) →
(∏t‘∅) ∈ Top) |
36 | 33, 34, 35 | mp2an 708 |
. . . . . . . 8
⊢
(∏t‘∅) ∈ Top |
37 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(∏t‘∅) =
(∏t‘∅) |
38 | 37 | ptuni 21397 |
. . . . . . . . . . . 12
⊢ ((∅
∈ V ∧ ∅:∅⟶Top) → X𝑥 ∈ ∅ ∪ (∅‘𝑥) = ∪
(∏t‘∅)) |
39 | 33, 34, 38 | mp2an 708 |
. . . . . . . . . . 11
⊢ X𝑥 ∈
∅ ∪ (∅‘𝑥) = ∪
(∏t‘∅) |
40 | | ixp0x 7936 |
. . . . . . . . . . . 12
⊢ X𝑥 ∈
∅ ∪ (∅‘𝑥) = {∅} |
41 | | snfi 8038 |
. . . . . . . . . . . 12
⊢ {∅}
∈ Fin |
42 | 40, 41 | eqeltri 2697 |
. . . . . . . . . . 11
⊢ X𝑥 ∈
∅ ∪ (∅‘𝑥) ∈ Fin |
43 | 39, 42 | eqeltrri 2698 |
. . . . . . . . . 10
⊢ ∪ (∏t‘∅) ∈
Fin |
44 | | pwfi 8261 |
. . . . . . . . . 10
⊢ (∪ (∏t‘∅) ∈ Fin ↔
𝒫 ∪ (∏t‘∅)
∈ Fin) |
45 | 43, 44 | mpbi 220 |
. . . . . . . . 9
⊢ 𝒫
∪ (∏t‘∅) ∈
Fin |
46 | | pwuni 4474 |
. . . . . . . . 9
⊢
(∏t‘∅) ⊆ 𝒫 ∪ (∏t‘∅) |
47 | | ssfi 8180 |
. . . . . . . . 9
⊢
((𝒫 ∪
(∏t‘∅) ∈ Fin ∧
(∏t‘∅) ⊆ 𝒫 ∪ (∏t‘∅)) →
(∏t‘∅) ∈ Fin) |
48 | 45, 46, 47 | mp2an 708 |
. . . . . . . 8
⊢
(∏t‘∅) ∈ Fin |
49 | | elin 3796 |
. . . . . . . 8
⊢
((∏t‘∅) ∈ (Top ∩ Fin) ↔
((∏t‘∅) ∈ Top ∧
(∏t‘∅) ∈ Fin)) |
50 | 36, 48, 49 | mpbir2an 955 |
. . . . . . 7
⊢
(∏t‘∅) ∈ (Top ∩
Fin) |
51 | | fincmp 21196 |
. . . . . . 7
⊢
((∏t‘∅) ∈ (Top ∩ Fin) →
(∏t‘∅) ∈ Comp) |
52 | 50, 51 | ax-mp 5 |
. . . . . 6
⊢
(∏t‘∅) ∈ Comp |
53 | 52 | 2a1i 12 |
. . . . 5
⊢ (∅
⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘∅) ∈ Comp)) |
54 | | ssun1 3776 |
. . . . . . . . 9
⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧}) |
55 | | id 22 |
. . . . . . . . 9
⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝑦 ∪ {𝑧}) ⊆ 𝐴) |
56 | 54, 55 | syl5ss 3614 |
. . . . . . . 8
⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → 𝑦 ⊆ 𝐴) |
57 | 56 | imim1i 63 |
. . . . . . 7
⊢ ((𝑦 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ 𝑦)) ∈ Comp))) |
58 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ ∪ (∏t‘(𝐹 ↾ 𝑦)) = ∪
(∏t‘(𝐹 ↾ 𝑦)) |
59 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ ∪ (∏t‘(𝐹 ↾ {𝑧})) = ∪
(∏t‘(𝐹 ↾ {𝑧})) |
60 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) = (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) |
61 | | resabs1 5427 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ⊆ (𝑦 ∪ {𝑧}) → ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦) = (𝐹 ↾ 𝑦)) |
62 | 54, 61 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦) = (𝐹 ↾ 𝑦) |
63 | 62 | eqcomi 2631 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ↾ 𝑦) = ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦) |
64 | 63 | fveq2i 6194 |
. . . . . . . . . . . . . 14
⊢
(∏t‘(𝐹 ↾ 𝑦)) = (∏t‘((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦)) |
65 | | ssun2 3777 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑧} ⊆ (𝑦 ∪ {𝑧}) |
66 | | resabs1 5427 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑧} ⊆ (𝑦 ∪ {𝑧}) → ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧}) = (𝐹 ↾ {𝑧})) |
67 | 65, 66 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧}) = (𝐹 ↾ {𝑧}) |
68 | 67 | eqcomi 2631 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ↾ {𝑧}) = ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧}) |
69 | 68 | fveq2i 6194 |
. . . . . . . . . . . . . 14
⊢
(∏t‘(𝐹 ↾ {𝑧})) = (∏t‘((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧})) |
70 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈ ∪ (∏t‘(𝐹 ↾ 𝑦)), 𝑣 ∈ ∪
(∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢 ∪ 𝑣)) = (𝑢 ∈ ∪
(∏t‘(𝐹 ↾ 𝑦)), 𝑣 ∈ ∪
(∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢 ∪ 𝑣)) |
71 | | vex 3203 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ∈ V |
72 | | snex 4908 |
. . . . . . . . . . . . . . . 16
⊢ {𝑧} ∈ V |
73 | 71, 72 | unex 6956 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∪ {𝑧}) ∈ V |
74 | 73 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) ∈ V) |
75 | | simplr 792 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝐹:𝐴⟶Comp) |
76 | | cmptop 21198 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ Comp → 𝑥 ∈ Top) |
77 | 76 | ssriv 3607 |
. . . . . . . . . . . . . . . 16
⊢ Comp
⊆ Top |
78 | | fss 6056 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝐴⟶Comp ∧ Comp ⊆ Top) →
𝐹:𝐴⟶Top) |
79 | 75, 77, 78 | sylancl 694 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝐹:𝐴⟶Top) |
80 | | simprr 796 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) ⊆ 𝐴) |
81 | 79, 80 | fssresd 6071 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹 ↾ (𝑦 ∪ {𝑧})):(𝑦 ∪ {𝑧})⟶Top) |
82 | | eqidd 2623 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) = (𝑦 ∪ {𝑧})) |
83 | | simprl 794 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ¬ 𝑧 ∈ 𝑦) |
84 | | disjsn 4246 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦) |
85 | 83, 84 | sylibr 224 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∩ {𝑧}) = ∅) |
86 | 58, 59, 60, 64, 69, 70, 74, 81, 82, 85 | ptunhmeo 21611 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑢 ∈ ∪
(∏t‘(𝐹 ↾ 𝑦)), 𝑣 ∈ ∪
(∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢 ∪ 𝑣)) ∈ (((∏t‘(𝐹 ↾ 𝑦)) ×t
(∏t‘(𝐹 ↾ {𝑧})))Homeo(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))))) |
87 | | hmphi 21580 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ ∪ (∏t‘(𝐹 ↾ 𝑦)), 𝑣 ∈ ∪
(∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢 ∪ 𝑣)) ∈ (((∏t‘(𝐹 ↾ 𝑦)) ×t
(∏t‘(𝐹 ↾ {𝑧})))Homeo(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧})))) →
((∏t‘(𝐹 ↾ 𝑦)) ×t
(∏t‘(𝐹 ↾ {𝑧}))) ≃ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧})))) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ((∏t‘(𝐹 ↾ 𝑦)) ×t
(∏t‘(𝐹 ↾ {𝑧}))) ≃ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧})))) |
89 | 1 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝐹 Fn 𝐴) |
90 | 65, 80 | syl5ss 3614 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → {𝑧} ⊆ 𝐴) |
91 | | vex 3203 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑧 ∈ V |
92 | 91 | snss 4316 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝐴 ↔ {𝑧} ⊆ 𝐴) |
93 | 90, 92 | sylibr 224 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧 ∈ 𝐴) |
94 | | fnressn 6425 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 Fn 𝐴 ∧ 𝑧 ∈ 𝐴) → (𝐹 ↾ {𝑧}) = {〈𝑧, (𝐹‘𝑧)〉}) |
95 | 89, 93, 94 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹 ↾ {𝑧}) = {〈𝑧, (𝐹‘𝑧)〉}) |
96 | 95 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (∏t‘(𝐹 ↾ {𝑧})) = (∏t‘{〈𝑧, (𝐹‘𝑧)〉})) |
97 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢
(∏t‘{〈𝑧, (𝐹‘𝑧)〉}) =
(∏t‘{〈𝑧, (𝐹‘𝑧)〉}) |
98 | 91 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧 ∈ V) |
99 | 75, 93 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹‘𝑧) ∈ Comp) |
100 | 77, 99 | sseldi 3601 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹‘𝑧) ∈ Top) |
101 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢ ∪ (𝐹‘𝑧) = ∪ (𝐹‘𝑧) |
102 | 101 | toptopon 20722 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑧) ∈ Top ↔ (𝐹‘𝑧) ∈ (TopOn‘∪ (𝐹‘𝑧))) |
103 | 100, 102 | sylib 208 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹‘𝑧) ∈ (TopOn‘∪ (𝐹‘𝑧))) |
104 | 97, 98, 103 | pt1hmeo 21609 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑥 ∈ ∪ (𝐹‘𝑧) ↦ {〈𝑧, 𝑥〉}) ∈ ((𝐹‘𝑧)Homeo(∏t‘{〈𝑧, (𝐹‘𝑧)〉}))) |
105 | | hmphi 21580 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ∪ (𝐹‘𝑧) ↦ {〈𝑧, 𝑥〉}) ∈ ((𝐹‘𝑧)Homeo(∏t‘{〈𝑧, (𝐹‘𝑧)〉})) → (𝐹‘𝑧) ≃
(∏t‘{〈𝑧, (𝐹‘𝑧)〉})) |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹‘𝑧) ≃
(∏t‘{〈𝑧, (𝐹‘𝑧)〉})) |
107 | | cmphmph 21591 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑧) ≃
(∏t‘{〈𝑧, (𝐹‘𝑧)〉}) → ((𝐹‘𝑧) ∈ Comp →
(∏t‘{〈𝑧, (𝐹‘𝑧)〉}) ∈ Comp)) |
108 | 106, 99, 107 | sylc 65 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) →
(∏t‘{〈𝑧, (𝐹‘𝑧)〉}) ∈ Comp) |
109 | 96, 108 | eqeltrd 2701 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (∏t‘(𝐹 ↾ {𝑧})) ∈ Comp) |
110 | | txcmp 21446 |
. . . . . . . . . . . . . 14
⊢
(((∏t‘(𝐹 ↾ 𝑦)) ∈ Comp ∧
(∏t‘(𝐹 ↾ {𝑧})) ∈ Comp) →
((∏t‘(𝐹 ↾ 𝑦)) ×t
(∏t‘(𝐹 ↾ {𝑧}))) ∈ Comp) |
111 | 110 | expcom 451 |
. . . . . . . . . . . . 13
⊢
((∏t‘(𝐹 ↾ {𝑧})) ∈ Comp →
((∏t‘(𝐹 ↾ 𝑦)) ∈ Comp →
((∏t‘(𝐹 ↾ 𝑦)) ×t
(∏t‘(𝐹 ↾ {𝑧}))) ∈ Comp)) |
112 | 109, 111 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ((∏t‘(𝐹 ↾ 𝑦)) ∈ Comp →
((∏t‘(𝐹 ↾ 𝑦)) ×t
(∏t‘(𝐹 ↾ {𝑧}))) ∈ Comp)) |
113 | | cmphmph 21591 |
. . . . . . . . . . . 12
⊢
(((∏t‘(𝐹 ↾ 𝑦)) ×t
(∏t‘(𝐹 ↾ {𝑧}))) ≃ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) →
(((∏t‘(𝐹 ↾ 𝑦)) ×t
(∏t‘(𝐹 ↾ {𝑧}))) ∈ Comp →
(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)) |
114 | 88, 112, 113 | sylsyld 61 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ((∏t‘(𝐹 ↾ 𝑦)) ∈ Comp →
(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)) |
115 | 114 | expcom 451 |
. . . . . . . . . 10
⊢ ((¬
𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
((∏t‘(𝐹 ↾ 𝑦)) ∈ Comp →
(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))) |
116 | 115 | a2d 29 |
. . . . . . . . 9
⊢ ((¬
𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ 𝑦)) ∈ Comp) → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))) |
117 | 116 | ex 450 |
. . . . . . . 8
⊢ (¬
𝑧 ∈ 𝑦 → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ 𝑦)) ∈ Comp) → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)))) |
118 | 117 | a2d 29 |
. . . . . . 7
⊢ (¬
𝑧 ∈ 𝑦 → (((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)))) |
119 | 57, 118 | syl5 34 |
. . . . . 6
⊢ (¬
𝑧 ∈ 𝑦 → ((𝑦 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)))) |
120 | 119 | adantl 482 |
. . . . 5
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝑦 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)))) |
121 | 14, 20, 26, 32, 53, 120 | findcard2s 8201 |
. . . 4
⊢ (𝐴 ∈ Fin → (𝐴 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ 𝐴)) ∈ Comp))) |
122 | 6, 121 | mpi 20 |
. . 3
⊢ (𝐴 ∈ Fin → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ 𝐴)) ∈ Comp)) |
123 | 122 | anabsi5 858 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘(𝐹 ↾ 𝐴)) ∈ Comp) |
124 | 5, 123 | eqeltrrd 2702 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) →
(∏t‘𝐹) ∈ Comp) |