Step | Hyp | Ref
| Expression |
1 | | ssid 3899 |
. 2
⊢ 𝐴 ⊆ 𝐴 |
2 | | simp2 1138 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → 𝐴 ∈ Fin) |
3 | | sseq1 3902 |
. . . . . 6
⊢ (𝑡 = ∅ → (𝑡 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴)) |
4 | | iuneq1 4897 |
. . . . . . . . 9
⊢ (𝑡 = ∅ → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ ∅ 𝐵) |
5 | | 0iun 4948 |
. . . . . . . . 9
⊢ ∪ 𝑥 ∈ ∅ 𝐵 = ∅ |
6 | 4, 5 | eqtrdi 2789 |
. . . . . . . 8
⊢ (𝑡 = ∅ → ∪ 𝑥 ∈ 𝑡 𝐵 = ∅) |
7 | 6 | oveq2d 7188 |
. . . . . . 7
⊢ (𝑡 = ∅ → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾t
∅)) |
8 | 7 | eleq1d 2817 |
. . . . . 6
⊢ (𝑡 = ∅ → ((𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾t ∅) ∈
Comp)) |
9 | 3, 8 | imbi12d 348 |
. . . . 5
⊢ (𝑡 = ∅ → ((𝑡 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ (∅ ⊆ 𝐴 → (𝐽 ↾t ∅) ∈
Comp))) |
10 | 9 | imbi2d 344 |
. . . 4
⊢ (𝑡 = ∅ → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (∅ ⊆ 𝐴 → (𝐽 ↾t ∅) ∈
Comp)))) |
11 | | sseq1 3902 |
. . . . . 6
⊢ (𝑡 = 𝑦 → (𝑡 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴)) |
12 | | iuneq1 4897 |
. . . . . . . 8
⊢ (𝑡 = 𝑦 → ∪
𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ 𝑦 𝐵) |
13 | 12 | oveq2d 7188 |
. . . . . . 7
⊢ (𝑡 = 𝑦 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵)) |
14 | 13 | eleq1d 2817 |
. . . . . 6
⊢ (𝑡 = 𝑦 → ((𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) |
15 | 11, 14 | imbi12d 348 |
. . . . 5
⊢ (𝑡 = 𝑦 → ((𝑡 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ (𝑦 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp))) |
16 | 15 | imbi2d 344 |
. . . 4
⊢ (𝑡 = 𝑦 → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝑦 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)))) |
17 | | sseq1 3902 |
. . . . . 6
⊢ (𝑡 = (𝑦 ∪ {𝑧}) → (𝑡 ⊆ 𝐴 ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) |
18 | | iuneq1 4897 |
. . . . . . . 8
⊢ (𝑡 = (𝑦 ∪ {𝑧}) → ∪
𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) |
19 | 18 | oveq2d 7188 |
. . . . . . 7
⊢ (𝑡 = (𝑦 ∪ {𝑧}) → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)) |
20 | 19 | eleq1d 2817 |
. . . . . 6
⊢ (𝑡 = (𝑦 ∪ {𝑧}) → ((𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)) |
21 | 17, 20 | imbi12d 348 |
. . . . 5
⊢ (𝑡 = (𝑦 ∪ {𝑧}) → ((𝑡 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp))) |
22 | 21 | imbi2d 344 |
. . . 4
⊢ (𝑡 = (𝑦 ∪ {𝑧}) → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)))) |
23 | | sseq1 3902 |
. . . . . 6
⊢ (𝑡 = 𝐴 → (𝑡 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴)) |
24 | | iuneq1 4897 |
. . . . . . . 8
⊢ (𝑡 = 𝐴 → ∪
𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵) |
25 | 24 | oveq2d 7188 |
. . . . . . 7
⊢ (𝑡 = 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵)) |
26 | 25 | eleq1d 2817 |
. . . . . 6
⊢ (𝑡 = 𝐴 → ((𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp)) |
27 | 23, 26 | imbi12d 348 |
. . . . 5
⊢ (𝑡 = 𝐴 → ((𝑡 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ (𝐴 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp))) |
28 | 27 | imbi2d 344 |
. . . 4
⊢ (𝑡 = 𝐴 → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝐴 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp)))) |
29 | | rest0 21922 |
. . . . . . 7
⊢ (𝐽 ∈ Top → (𝐽 ↾t ∅) =
{∅}) |
30 | | 0cmp 22147 |
. . . . . . 7
⊢ {∅}
∈ Comp |
31 | 29, 30 | eqeltrdi 2841 |
. . . . . 6
⊢ (𝐽 ∈ Top → (𝐽 ↾t ∅)
∈ Comp) |
32 | 31 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝐽 ↾t ∅) ∈
Comp) |
33 | 32 | a1d 25 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (∅ ⊆ 𝐴 → (𝐽 ↾t ∅) ∈
Comp)) |
34 | | ssun1 4062 |
. . . . . . . . 9
⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧}) |
35 | | id 22 |
. . . . . . . . 9
⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝑦 ∪ {𝑧}) ⊆ 𝐴) |
36 | 34, 35 | sstrid 3888 |
. . . . . . . 8
⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → 𝑦 ⊆ 𝐴) |
37 | 36 | imim1i 63 |
. . . . . . 7
⊢ ((𝑦 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) |
38 | | simpl1 1192 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → 𝐽 ∈ Top) |
39 | | iunxun 4979 |
. . . . . . . . . . . 12
⊢ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 = (∪
𝑥 ∈ 𝑦 𝐵 ∪ ∪
𝑥 ∈ {𝑧}𝐵) |
40 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp) |
41 | | cmptop 22148 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Top) |
42 | | restrcl 21910 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Top → (𝐽 ∈ V ∧ ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V)) |
43 | 42 | simprd 499 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Top → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V) |
44 | 40, 41, 43 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V) |
45 | | nfcv 2899 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑡𝐵 |
46 | | nfcsb1v 3814 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥⦋𝑡 / 𝑥⦌𝐵 |
47 | | csbeq1a 3804 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑡 → 𝐵 = ⦋𝑡 / 𝑥⦌𝐵) |
48 | 45, 46, 47 | cbviun 4922 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑥 ∈ {𝑧}𝐵 = ∪ 𝑡 ∈ {𝑧}⦋𝑡 / 𝑥⦌𝐵 |
49 | | vex 3402 |
. . . . . . . . . . . . . . . 16
⊢ 𝑧 ∈ V |
50 | | csbeq1 3793 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑧 → ⦋𝑡 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
51 | 49, 50 | iunxsn 4976 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑡 ∈ {𝑧}⦋𝑡 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵 |
52 | 48, 51 | eqtri 2761 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑥 ∈ {𝑧}𝐵 = ⦋𝑧 / 𝑥⦌𝐵 |
53 | 50 | oveq2d 7188 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑧 → (𝐽 ↾t ⦋𝑡 / 𝑥⦌𝐵) = (𝐽 ↾t ⦋𝑧 / 𝑥⦌𝐵)) |
54 | 53 | eleq1d 2817 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑧 → ((𝐽 ↾t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp ↔ (𝐽 ↾t ⦋𝑧 / 𝑥⦌𝐵) ∈ Comp)) |
55 | | simpl3 1194 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) |
56 | | nfv 1921 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡(𝐽 ↾t 𝐵) ∈ Comp |
57 | | nfcv 2899 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥𝐽 |
58 | | nfcv 2899 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥
↾t |
59 | 57, 58, 46 | nfov 7202 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝐽 ↾t ⦋𝑡 / 𝑥⦌𝐵) |
60 | 59 | nfel1 2915 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥(𝐽 ↾t
⦋𝑡 / 𝑥⦌𝐵) ∈ Comp |
61 | 47 | oveq2d 7188 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑡 → (𝐽 ↾t 𝐵) = (𝐽 ↾t ⦋𝑡 / 𝑥⦌𝐵)) |
62 | 61 | eleq1d 2817 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑡 → ((𝐽 ↾t 𝐵) ∈ Comp ↔ (𝐽 ↾t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp)) |
63 | 56, 60, 62 | cbvralw 3340 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑥 ∈
𝐴 (𝐽 ↾t 𝐵) ∈ Comp ↔ ∀𝑡 ∈ 𝐴 (𝐽 ↾t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp) |
64 | 55, 63 | sylib 221 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∀𝑡 ∈ 𝐴 (𝐽 ↾t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp) |
65 | | ssun2 4063 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑧} ⊆ (𝑦 ∪ {𝑧}) |
66 | | simprl 771 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝑦 ∪ {𝑧}) ⊆ 𝐴) |
67 | 65, 66 | sstrid 3888 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → {𝑧} ⊆ 𝐴) |
68 | 49 | snss 4674 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝐴 ↔ {𝑧} ⊆ 𝐴) |
69 | 67, 68 | sylibr 237 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → 𝑧 ∈ 𝐴) |
70 | 54, 64, 69 | rspcdva 3528 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾t ⦋𝑧 / 𝑥⦌𝐵) ∈ Comp) |
71 | | cmptop 22148 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ↾t
⦋𝑧 / 𝑥⦌𝐵) ∈ Comp → (𝐽 ↾t ⦋𝑧 / 𝑥⦌𝐵) ∈ Top) |
72 | | restrcl 21910 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ↾t
⦋𝑧 / 𝑥⦌𝐵) ∈ Top → (𝐽 ∈ V ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ V)) |
73 | 72 | simprd 499 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ↾t
⦋𝑧 / 𝑥⦌𝐵) ∈ Top → ⦋𝑧 / 𝑥⦌𝐵 ∈ V) |
74 | 70, 71, 73 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ⦋𝑧 / 𝑥⦌𝐵 ∈ V) |
75 | 52, 74 | eqeltrid 2837 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ 𝑥 ∈ {𝑧}𝐵 ∈ V) |
76 | | unexg 7492 |
. . . . . . . . . . . . 13
⊢
((∪ 𝑥 ∈ 𝑦 𝐵 ∈ V ∧ ∪ 𝑥 ∈ {𝑧}𝐵 ∈ V) → (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪
𝑥 ∈ {𝑧}𝐵) ∈ V) |
77 | 44, 75, 76 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪
𝑥 ∈ {𝑧}𝐵) ∈ V) |
78 | 39, 77 | eqeltrid 2837 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) |
79 | | resttop 21913 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Top) |
80 | 38, 78, 79 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Top) |
81 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝐽 =
∪ 𝐽 |
82 | 81 | restin 21919 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = (𝐽 ↾t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽))) |
83 | 38, 78, 82 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = (𝐽 ↾t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽))) |
84 | 83 | unieqd 4810 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ (𝐽
↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ∪ (𝐽 ↾t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽))) |
85 | | inss2 4120 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝐽 |
86 | | fiuncmp.1 |
. . . . . . . . . . . . . 14
⊢ 𝑋 = ∪
𝐽 |
87 | 85, 86 | sseqtrri 3914 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) ⊆ 𝑋 |
88 | 86 | restuni 21915 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) ⊆ 𝑋) → (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ∪
(𝐽 ↾t
(∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽))) |
89 | 38, 87, 88 | sylancl 589 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ∪
(𝐽 ↾t
(∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽))) |
90 | 84, 89 | eqtr4d 2776 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ (𝐽
↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = (∪
𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)) |
91 | 52 | uneq2i 4050 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪
𝑥 ∈ {𝑧}𝐵) = (∪
𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵) |
92 | 39, 91 | eqtri 2761 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 = (∪
𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵) |
93 | 92 | ineq1i 4099 |
. . . . . . . . . . . 12
⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵) ∩ ∪ 𝐽) |
94 | | indir 4166 |
. . . . . . . . . . . 12
⊢
((∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵) ∩ ∪ 𝐽) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) |
95 | 93, 94 | eqtri 2761 |
. . . . . . . . . . 11
⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) |
96 | 90, 95 | eqtrdi 2789 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ (𝐽
↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ((∪
𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))) |
97 | | inss1 4119 |
. . . . . . . . . . . . . . 15
⊢ (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ 𝑦 𝐵 |
98 | | ssun1 4062 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪
𝑥 ∈ {𝑧}𝐵) |
99 | 98, 39 | sseqtrri 3914 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ∪
𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 |
100 | 97, 99 | sstri 3886 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 |
101 | 100 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) |
102 | | restabs 21918 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∧ ∪
𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽))) |
103 | 38, 101, 78, 102 | syl3anc 1372 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽))) |
104 | 81 | restin 21919 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V) → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) = (𝐽 ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽))) |
105 | 38, 44, 104 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) = (𝐽 ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽))) |
106 | 103, 105 | eqtr4d 2776 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵)) |
107 | 106, 40 | eqeltrd 2833 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) ∈ Comp) |
108 | | inss1 4119 |
. . . . . . . . . . . . . . 15
⊢
(⦋𝑧 /
𝑥⦌𝐵 ∩ ∪ 𝐽)
⊆ ⦋𝑧 /
𝑥⦌𝐵 |
109 | | ssun2 4063 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑥 ∈ {𝑧}𝐵 ⊆ (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪
𝑥 ∈ {𝑧}𝐵) |
110 | 109, 39 | sseqtrri 3914 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑥 ∈ {𝑧}𝐵 ⊆ ∪
𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 |
111 | 52, 110 | eqsstrri 3912 |
. . . . . . . . . . . . . . 15
⊢
⦋𝑧 /
𝑥⦌𝐵 ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 |
112 | 108, 111 | sstri 3886 |
. . . . . . . . . . . . . 14
⊢
(⦋𝑧 /
𝑥⦌𝐵 ∩ ∪ 𝐽)
⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 |
113 | 112 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) |
114 | | restabs 21918 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧
(⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∧ ∪
𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))) |
115 | 38, 113, 78, 114 | syl3anc 1372 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))) |
116 | 81 | restin 21919 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧
⦋𝑧 / 𝑥⦌𝐵 ∈ V) → (𝐽 ↾t ⦋𝑧 / 𝑥⦌𝐵) = (𝐽 ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))) |
117 | 38, 74, 116 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾t ⦋𝑧 / 𝑥⦌𝐵) = (𝐽 ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))) |
118 | 115, 117 | eqtr4d 2776 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾t ⦋𝑧 / 𝑥⦌𝐵)) |
119 | 118, 70 | eqeltrd 2833 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) ∈ Comp) |
120 | | eqid 2738 |
. . . . . . . . . . 11
⊢ ∪ (𝐽
↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ∪ (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) |
121 | 120 | uncmp 22156 |
. . . . . . . . . 10
⊢ ((((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Top ∧ ∪ (𝐽
↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ((∪
𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))) ∧ (((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) ∈ Comp ∧ ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) ∈ Comp)) → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp) |
122 | 80, 96, 107, 119, 121 | syl22anc 838 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp) |
123 | 122 | exp32 424 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp))) |
124 | 123 | a2d 29 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp))) |
125 | 37, 124 | syl5 34 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → ((𝑦 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp))) |
126 | 125 | a2i 14 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝑦 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp))) |
127 | 126 | a1i 11 |
. . . 4
⊢ (𝑦 ∈ Fin → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝑦 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)))) |
128 | 10, 16, 22, 28, 33, 127 | findcard2 8765 |
. . 3
⊢ (𝐴 ∈ Fin → ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝐴 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp))) |
129 | 2, 128 | mpcom 38 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝐴 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp)) |
130 | 1, 129 | mpi 20 |
1
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp) |