Step | Hyp | Ref
| Expression |
1 | | ssid 3587 |
. 2
⊢ 𝐴 ⊆ 𝐴 |
2 | | simp2 1055 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → 𝐴 ∈ Fin) |
3 | | sseq1 3589 |
. . . . . 6
⊢ (𝑡 = ∅ → (𝑡 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴)) |
4 | | iuneq1 4470 |
. . . . . . . . 9
⊢ (𝑡 = ∅ → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ ∅ 𝐵) |
5 | | 0iun 4513 |
. . . . . . . . 9
⊢ ∪ 𝑥 ∈ ∅ 𝐵 = ∅ |
6 | 4, 5 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝑡 = ∅ → ∪ 𝑥 ∈ 𝑡 𝐵 = ∅) |
7 | 6 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑡 = ∅ → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾t
∅)) |
8 | 7 | eleq1d 2672 |
. . . . . 6
⊢ (𝑡 = ∅ → ((𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾t ∅) ∈
Comp)) |
9 | 3, 8 | imbi12d 333 |
. . . . 5
⊢ (𝑡 = ∅ → ((𝑡 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ (∅ ⊆ 𝐴 → (𝐽 ↾t ∅) ∈
Comp))) |
10 | 9 | imbi2d 329 |
. . . 4
⊢ (𝑡 = ∅ → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (∅ ⊆ 𝐴 → (𝐽 ↾t ∅) ∈
Comp)))) |
11 | | sseq1 3589 |
. . . . . 6
⊢ (𝑡 = 𝑦 → (𝑡 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴)) |
12 | | iuneq1 4470 |
. . . . . . . 8
⊢ (𝑡 = 𝑦 → ∪
𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ 𝑦 𝐵) |
13 | 12 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑡 = 𝑦 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵)) |
14 | 13 | eleq1d 2672 |
. . . . . 6
⊢ (𝑡 = 𝑦 → ((𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) |
15 | 11, 14 | imbi12d 333 |
. . . . 5
⊢ (𝑡 = 𝑦 → ((𝑡 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ (𝑦 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp))) |
16 | 15 | imbi2d 329 |
. . . 4
⊢ (𝑡 = 𝑦 → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝑦 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)))) |
17 | | sseq1 3589 |
. . . . . 6
⊢ (𝑡 = (𝑦 ∪ {𝑧}) → (𝑡 ⊆ 𝐴 ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) |
18 | | iuneq1 4470 |
. . . . . . . 8
⊢ (𝑡 = (𝑦 ∪ {𝑧}) → ∪
𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) |
19 | 18 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑡 = (𝑦 ∪ {𝑧}) → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)) |
20 | 19 | eleq1d 2672 |
. . . . . 6
⊢ (𝑡 = (𝑦 ∪ {𝑧}) → ((𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)) |
21 | 17, 20 | imbi12d 333 |
. . . . 5
⊢ (𝑡 = (𝑦 ∪ {𝑧}) → ((𝑡 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp))) |
22 | 21 | imbi2d 329 |
. . . 4
⊢ (𝑡 = (𝑦 ∪ {𝑧}) → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)))) |
23 | | sseq1 3589 |
. . . . . 6
⊢ (𝑡 = 𝐴 → (𝑡 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴)) |
24 | | iuneq1 4470 |
. . . . . . . 8
⊢ (𝑡 = 𝐴 → ∪
𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵) |
25 | 24 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑡 = 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵)) |
26 | 25 | eleq1d 2672 |
. . . . . 6
⊢ (𝑡 = 𝐴 → ((𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp)) |
27 | 23, 26 | imbi12d 333 |
. . . . 5
⊢ (𝑡 = 𝐴 → ((𝑡 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ (𝐴 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp))) |
28 | 27 | imbi2d 329 |
. . . 4
⊢ (𝑡 = 𝐴 → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝐴 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp)))) |
29 | | rest0 20783 |
. . . . . . 7
⊢ (𝐽 ∈ Top → (𝐽 ↾t ∅) =
{∅}) |
30 | | 0cmp 21007 |
. . . . . . 7
⊢ {∅}
∈ Comp |
31 | 29, 30 | syl6eqel 2696 |
. . . . . 6
⊢ (𝐽 ∈ Top → (𝐽 ↾t ∅)
∈ Comp) |
32 | 31 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝐽 ↾t ∅) ∈
Comp) |
33 | 32 | a1d 25 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (∅ ⊆ 𝐴 → (𝐽 ↾t ∅) ∈
Comp)) |
34 | | ssun1 3738 |
. . . . . . . . 9
⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧}) |
35 | | id 22 |
. . . . . . . . 9
⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝑦 ∪ {𝑧}) ⊆ 𝐴) |
36 | 34, 35 | syl5ss 3579 |
. . . . . . . 8
⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → 𝑦 ⊆ 𝐴) |
37 | 36 | imim1i 61 |
. . . . . . 7
⊢ ((𝑦 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) |
38 | | simpl1 1057 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → 𝐽 ∈ Top) |
39 | | iunxun 4541 |
. . . . . . . . . . . 12
⊢ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 = (∪
𝑥 ∈ 𝑦 𝐵 ∪ ∪
𝑥 ∈ {𝑧}𝐵) |
40 | | simprr 792 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp) |
41 | | cmptop 21008 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Top) |
42 | | restrcl 20771 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Top → (𝐽 ∈ V ∧ ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V)) |
43 | 42 | simprd 478 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Top → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V) |
44 | 40, 41, 43 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V) |
45 | | nfcv 2751 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑡𝐵 |
46 | | nfcsb1v 3515 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥⦋𝑡 / 𝑥⦌𝐵 |
47 | | csbeq1a 3508 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑡 → 𝐵 = ⦋𝑡 / 𝑥⦌𝐵) |
48 | 45, 46, 47 | cbviun 4493 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑥 ∈ {𝑧}𝐵 = ∪ 𝑡 ∈ {𝑧}⦋𝑡 / 𝑥⦌𝐵 |
49 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑧 ∈ V |
50 | | csbeq1 3502 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑧 → ⦋𝑡 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
51 | 49, 50 | iunxsn 4539 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑡 ∈ {𝑧}⦋𝑡 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵 |
52 | 48, 51 | eqtri 2632 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑥 ∈ {𝑧}𝐵 = ⦋𝑧 / 𝑥⦌𝐵 |
53 | | ssun2 3739 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑧} ⊆ (𝑦 ∪ {𝑧}) |
54 | | simprl 790 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝑦 ∪ {𝑧}) ⊆ 𝐴) |
55 | 53, 54 | syl5ss 3579 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → {𝑧} ⊆ 𝐴) |
56 | 49 | snss 4259 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝐴 ↔ {𝑧} ⊆ 𝐴) |
57 | 55, 56 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → 𝑧 ∈ 𝐴) |
58 | | simpl3 1059 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) |
59 | | nfv 1830 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡(𝐽 ↾t 𝐵) ∈ Comp |
60 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥𝐽 |
61 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥
↾t |
62 | 60, 61, 46 | nfov 6575 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝐽 ↾t ⦋𝑡 / 𝑥⦌𝐵) |
63 | 62 | nfel1 2765 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥(𝐽 ↾t
⦋𝑡 / 𝑥⦌𝐵) ∈ Comp |
64 | 47 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑡 → (𝐽 ↾t 𝐵) = (𝐽 ↾t ⦋𝑡 / 𝑥⦌𝐵)) |
65 | 64 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑡 → ((𝐽 ↾t 𝐵) ∈ Comp ↔ (𝐽 ↾t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp)) |
66 | 59, 63, 65 | cbvral 3143 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑥 ∈
𝐴 (𝐽 ↾t 𝐵) ∈ Comp ↔ ∀𝑡 ∈ 𝐴 (𝐽 ↾t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp) |
67 | 58, 66 | sylib 207 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∀𝑡 ∈ 𝐴 (𝐽 ↾t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp) |
68 | 50 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑧 → (𝐽 ↾t ⦋𝑡 / 𝑥⦌𝐵) = (𝐽 ↾t ⦋𝑧 / 𝑥⦌𝐵)) |
69 | 68 | eleq1d 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑧 → ((𝐽 ↾t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp ↔ (𝐽 ↾t ⦋𝑧 / 𝑥⦌𝐵) ∈ Comp)) |
70 | 69 | rspcv 3278 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝐴 → (∀𝑡 ∈ 𝐴 (𝐽 ↾t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp → (𝐽 ↾t ⦋𝑧 / 𝑥⦌𝐵) ∈ Comp)) |
71 | 57, 67, 70 | sylc 63 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾t ⦋𝑧 / 𝑥⦌𝐵) ∈ Comp) |
72 | | cmptop 21008 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ↾t
⦋𝑧 / 𝑥⦌𝐵) ∈ Comp → (𝐽 ↾t ⦋𝑧 / 𝑥⦌𝐵) ∈ Top) |
73 | | restrcl 20771 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ↾t
⦋𝑧 / 𝑥⦌𝐵) ∈ Top → (𝐽 ∈ V ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ V)) |
74 | 73 | simprd 478 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ↾t
⦋𝑧 / 𝑥⦌𝐵) ∈ Top → ⦋𝑧 / 𝑥⦌𝐵 ∈ V) |
75 | 71, 72, 74 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ⦋𝑧 / 𝑥⦌𝐵 ∈ V) |
76 | 52, 75 | syl5eqel 2692 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ 𝑥 ∈ {𝑧}𝐵 ∈ V) |
77 | | unexg 6857 |
. . . . . . . . . . . . 13
⊢
((∪ 𝑥 ∈ 𝑦 𝐵 ∈ V ∧ ∪ 𝑥 ∈ {𝑧}𝐵 ∈ V) → (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪
𝑥 ∈ {𝑧}𝐵) ∈ V) |
78 | 44, 76, 77 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪
𝑥 ∈ {𝑧}𝐵) ∈ V) |
79 | 39, 78 | syl5eqel 2692 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) |
80 | | resttop 20774 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Top) |
81 | 38, 79, 80 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Top) |
82 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝐽 =
∪ 𝐽 |
83 | 82 | restin 20780 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = (𝐽 ↾t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽))) |
84 | 38, 79, 83 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = (𝐽 ↾t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽))) |
85 | 84 | unieqd 4382 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ (𝐽
↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ∪ (𝐽 ↾t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽))) |
86 | | inss2 3796 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝐽 |
87 | | fiuncmp.1 |
. . . . . . . . . . . . . 14
⊢ 𝑋 = ∪
𝐽 |
88 | 86, 87 | sseqtr4i 3601 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) ⊆ 𝑋 |
89 | 87 | restuni 20776 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) ⊆ 𝑋) → (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ∪
(𝐽 ↾t
(∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽))) |
90 | 38, 88, 89 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ∪
(𝐽 ↾t
(∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽))) |
91 | 85, 90 | eqtr4d 2647 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ (𝐽
↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = (∪
𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)) |
92 | 52 | uneq2i 3726 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪
𝑥 ∈ {𝑧}𝐵) = (∪
𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵) |
93 | 39, 92 | eqtri 2632 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 = (∪
𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵) |
94 | 93 | ineq1i 3772 |
. . . . . . . . . . . 12
⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵) ∩ ∪ 𝐽) |
95 | | indir 3834 |
. . . . . . . . . . . 12
⊢
((∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵) ∩ ∪ 𝐽) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) |
96 | 94, 95 | eqtri 2632 |
. . . . . . . . . . 11
⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) |
97 | 91, 96 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ (𝐽
↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ((∪
𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))) |
98 | | inss1 3795 |
. . . . . . . . . . . . . . 15
⊢ (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ 𝑦 𝐵 |
99 | | ssun1 3738 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪
𝑥 ∈ {𝑧}𝐵) |
100 | 99, 39 | sseqtr4i 3601 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ∪
𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 |
101 | 98, 100 | sstri 3577 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 |
102 | 101 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) |
103 | | restabs 20779 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∧ ∪
𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽))) |
104 | 38, 102, 79, 103 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽))) |
105 | 82 | restin 20780 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V) → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) = (𝐽 ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽))) |
106 | 38, 44, 105 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) = (𝐽 ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽))) |
107 | 104, 106 | eqtr4d 2647 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵)) |
108 | 107, 40 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) ∈ Comp) |
109 | | inss1 3795 |
. . . . . . . . . . . . . . 15
⊢
(⦋𝑧 /
𝑥⦌𝐵 ∩ ∪ 𝐽)
⊆ ⦋𝑧 /
𝑥⦌𝐵 |
110 | | ssun2 3739 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑥 ∈ {𝑧}𝐵 ⊆ (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪
𝑥 ∈ {𝑧}𝐵) |
111 | 110, 39 | sseqtr4i 3601 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑥 ∈ {𝑧}𝐵 ⊆ ∪
𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 |
112 | 52, 111 | eqsstr3i 3599 |
. . . . . . . . . . . . . . 15
⊢
⦋𝑧 /
𝑥⦌𝐵 ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 |
113 | 109, 112 | sstri 3577 |
. . . . . . . . . . . . . 14
⊢
(⦋𝑧 /
𝑥⦌𝐵 ∩ ∪ 𝐽)
⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 |
114 | 113 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) |
115 | | restabs 20779 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧
(⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∧ ∪
𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))) |
116 | 38, 114, 79, 115 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))) |
117 | 82 | restin 20780 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧
⦋𝑧 / 𝑥⦌𝐵 ∈ V) → (𝐽 ↾t ⦋𝑧 / 𝑥⦌𝐵) = (𝐽 ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))) |
118 | 38, 75, 117 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾t ⦋𝑧 / 𝑥⦌𝐵) = (𝐽 ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))) |
119 | 116, 118 | eqtr4d 2647 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾t ⦋𝑧 / 𝑥⦌𝐵)) |
120 | 119, 71 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) ∈ Comp) |
121 | | eqid 2610 |
. . . . . . . . . . 11
⊢ ∪ (𝐽
↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ∪ (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) |
122 | 121 | uncmp 21016 |
. . . . . . . . . 10
⊢ ((((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Top ∧ ∪ (𝐽
↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ((∪
𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))) ∧ (((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) ∈ Comp ∧ ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) ∈ Comp)) → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp) |
123 | 81, 97, 108, 120, 122 | syl22anc 1319 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp) |
124 | 123 | exp32 629 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp))) |
125 | 124 | a2d 29 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp))) |
126 | 37, 125 | syl5 33 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → ((𝑦 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp))) |
127 | 126 | a2i 14 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝑦 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp))) |
128 | 127 | a1i 11 |
. . . 4
⊢ (𝑦 ∈ Fin → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝑦 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)))) |
129 | 10, 16, 22, 28, 33, 128 | findcard2 8085 |
. . 3
⊢ (𝐴 ∈ Fin → ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝐴 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp))) |
130 | 2, 129 | mpcom 37 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝐴 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp)) |
131 | 1, 130 | mpi 20 |
1
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp) |