| Step | Hyp | Ref
| Expression |
| 1 | | ssid 4006 |
. 2
⊢ 𝐴 ⊆ 𝐴 |
| 2 | | simp2 1138 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → 𝐴 ∈ Fin) |
| 3 | | sseq1 4009 |
. . . . . 6
⊢ (𝑡 = ∅ → (𝑡 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴)) |
| 4 | | iuneq1 5008 |
. . . . . . . . 9
⊢ (𝑡 = ∅ → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ ∅ 𝐵) |
| 5 | | 0iun 5063 |
. . . . . . . . 9
⊢ ∪ 𝑥 ∈ ∅ 𝐵 = ∅ |
| 6 | 4, 5 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑡 = ∅ → ∪ 𝑥 ∈ 𝑡 𝐵 = ∅) |
| 7 | 6 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑡 = ∅ → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾t
∅)) |
| 8 | 7 | eleq1d 2826 |
. . . . . 6
⊢ (𝑡 = ∅ → ((𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾t ∅) ∈
Comp)) |
| 9 | 3, 8 | imbi12d 344 |
. . . . 5
⊢ (𝑡 = ∅ → ((𝑡 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ (∅ ⊆ 𝐴 → (𝐽 ↾t ∅) ∈
Comp))) |
| 10 | 9 | imbi2d 340 |
. . . 4
⊢ (𝑡 = ∅ → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (∅ ⊆ 𝐴 → (𝐽 ↾t ∅) ∈
Comp)))) |
| 11 | | sseq1 4009 |
. . . . . 6
⊢ (𝑡 = 𝑦 → (𝑡 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴)) |
| 12 | | iuneq1 5008 |
. . . . . . . 8
⊢ (𝑡 = 𝑦 → ∪
𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ 𝑦 𝐵) |
| 13 | 12 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑡 = 𝑦 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵)) |
| 14 | 13 | eleq1d 2826 |
. . . . . 6
⊢ (𝑡 = 𝑦 → ((𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) |
| 15 | 11, 14 | imbi12d 344 |
. . . . 5
⊢ (𝑡 = 𝑦 → ((𝑡 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ (𝑦 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp))) |
| 16 | 15 | imbi2d 340 |
. . . 4
⊢ (𝑡 = 𝑦 → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝑦 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)))) |
| 17 | | sseq1 4009 |
. . . . . 6
⊢ (𝑡 = (𝑦 ∪ {𝑧}) → (𝑡 ⊆ 𝐴 ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) |
| 18 | | iuneq1 5008 |
. . . . . . . 8
⊢ (𝑡 = (𝑦 ∪ {𝑧}) → ∪
𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) |
| 19 | 18 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑡 = (𝑦 ∪ {𝑧}) → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)) |
| 20 | 19 | eleq1d 2826 |
. . . . . 6
⊢ (𝑡 = (𝑦 ∪ {𝑧}) → ((𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)) |
| 21 | 17, 20 | imbi12d 344 |
. . . . 5
⊢ (𝑡 = (𝑦 ∪ {𝑧}) → ((𝑡 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp))) |
| 22 | 21 | imbi2d 340 |
. . . 4
⊢ (𝑡 = (𝑦 ∪ {𝑧}) → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)))) |
| 23 | | sseq1 4009 |
. . . . . 6
⊢ (𝑡 = 𝐴 → (𝑡 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴)) |
| 24 | | iuneq1 5008 |
. . . . . . . 8
⊢ (𝑡 = 𝐴 → ∪
𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵) |
| 25 | 24 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑡 = 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵)) |
| 26 | 25 | eleq1d 2826 |
. . . . . 6
⊢ (𝑡 = 𝐴 → ((𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp)) |
| 27 | 23, 26 | imbi12d 344 |
. . . . 5
⊢ (𝑡 = 𝐴 → ((𝑡 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ (𝐴 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp))) |
| 28 | 27 | imbi2d 340 |
. . . 4
⊢ (𝑡 = 𝐴 → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝐴 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp)))) |
| 29 | | rest0 23177 |
. . . . . . 7
⊢ (𝐽 ∈ Top → (𝐽 ↾t ∅) =
{∅}) |
| 30 | | 0cmp 23402 |
. . . . . . 7
⊢ {∅}
∈ Comp |
| 31 | 29, 30 | eqeltrdi 2849 |
. . . . . 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 4178 |
. . . . . . . . 9
⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧}) |
| 35 | | id 22 |
. . . . . . . . 9
⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝑦 ∪ {𝑧}) ⊆ 𝐴) |
| 36 | 34, 35 | sstrid 3995 |
. . . . . . . 8
⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → 𝑦 ⊆ 𝐴) |
| 37 | 36 | imim1i 63 |
. . . . . . 7
⊢ ((𝑦 ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) |
| 38 | | simpl1 1192 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → 𝐽 ∈ Top) |
| 39 | | iunxun 5094 |
. . . . . . . . . . . 12
⊢ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 = (∪
𝑥 ∈ 𝑦 𝐵 ∪ ∪
𝑥 ∈ {𝑧}𝐵) |
| 40 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp) |
| 41 | | cmptop 23403 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Top) |
| 42 | | restrcl 23165 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Top → (𝐽 ∈ V ∧ ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V)) |
| 43 | 42 | simprd 495 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Top → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V) |
| 44 | 40, 41, 43 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V) |
| 45 | | nfcv 2905 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑡𝐵 |
| 46 | | nfcsb1v 3923 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥⦋𝑡 / 𝑥⦌𝐵 |
| 47 | | csbeq1a 3913 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑡 → 𝐵 = ⦋𝑡 / 𝑥⦌𝐵) |
| 48 | 45, 46, 47 | cbviun 5036 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑥 ∈ {𝑧}𝐵 = ∪ 𝑡 ∈ {𝑧}⦋𝑡 / 𝑥⦌𝐵 |
| 49 | | vex 3484 |
. . . . . . . . . . . . . . . 16
⊢ 𝑧 ∈ V |
| 50 | | csbeq1 3902 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑧 → ⦋𝑡 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
| 51 | 49, 50 | iunxsn 5091 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑡 ∈ {𝑧}⦋𝑡 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵 |
| 52 | 48, 51 | eqtri 2765 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑥 ∈ {𝑧}𝐵 = ⦋𝑧 / 𝑥⦌𝐵 |
| 53 | 50 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑧 → (𝐽 ↾t ⦋𝑡 / 𝑥⦌𝐵) = (𝐽 ↾t ⦋𝑧 / 𝑥⦌𝐵)) |
| 54 | 53 | eleq1d 2826 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑧 → ((𝐽 ↾t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp ↔ (𝐽 ↾t ⦋𝑧 / 𝑥⦌𝐵) ∈ Comp)) |
| 55 | | simpl3 1194 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) |
| 56 | | nfv 1914 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡(𝐽 ↾t 𝐵) ∈ Comp |
| 57 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥𝐽 |
| 58 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥
↾t |
| 59 | 57, 58, 46 | nfov 7461 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝐽 ↾t ⦋𝑡 / 𝑥⦌𝐵) |
| 60 | 59 | nfel1 2922 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥(𝐽 ↾t
⦋𝑡 / 𝑥⦌𝐵) ∈ Comp |
| 61 | 47 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑡 → (𝐽 ↾t 𝐵) = (𝐽 ↾t ⦋𝑡 / 𝑥⦌𝐵)) |
| 62 | 61 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑡 → ((𝐽 ↾t 𝐵) ∈ Comp ↔ (𝐽 ↾t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp)) |
| 63 | 56, 60, 62 | cbvralw 3306 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑥 ∈
𝐴 (𝐽 ↾t 𝐵) ∈ Comp ↔ ∀𝑡 ∈ 𝐴 (𝐽 ↾t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp) |
| 64 | 55, 63 | sylib 218 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∀𝑡 ∈ 𝐴 (𝐽 ↾t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp) |
| 65 | | ssun2 4179 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑧} ⊆ (𝑦 ∪ {𝑧}) |
| 66 | | simprl 771 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝑦 ∪ {𝑧}) ⊆ 𝐴) |
| 67 | 65, 66 | sstrid 3995 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → {𝑧} ⊆ 𝐴) |
| 68 | 49 | snss 4785 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝐴 ↔ {𝑧} ⊆ 𝐴) |
| 69 | 67, 68 | sylibr 234 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → 𝑧 ∈ 𝐴) |
| 70 | 54, 64, 69 | rspcdva 3623 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾t ⦋𝑧 / 𝑥⦌𝐵) ∈ Comp) |
| 71 | | cmptop 23403 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ↾t
⦋𝑧 / 𝑥⦌𝐵) ∈ Comp → (𝐽 ↾t ⦋𝑧 / 𝑥⦌𝐵) ∈ Top) |
| 72 | | restrcl 23165 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ↾t
⦋𝑧 / 𝑥⦌𝐵) ∈ Top → (𝐽 ∈ V ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ V)) |
| 73 | 72 | simprd 495 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ↾t
⦋𝑧 / 𝑥⦌𝐵) ∈ Top → ⦋𝑧 / 𝑥⦌𝐵 ∈ V) |
| 74 | 70, 71, 73 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ⦋𝑧 / 𝑥⦌𝐵 ∈ V) |
| 75 | 52, 74 | eqeltrid 2845 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ 𝑥 ∈ {𝑧}𝐵 ∈ V) |
| 76 | | unexg 7763 |
. . . . . . . . . . . . 13
⊢
((∪ 𝑥 ∈ 𝑦 𝐵 ∈ V ∧ ∪ 𝑥 ∈ {𝑧}𝐵 ∈ V) → (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪
𝑥 ∈ {𝑧}𝐵) ∈ V) |
| 77 | 44, 75, 76 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪
𝑥 ∈ {𝑧}𝐵) ∈ V) |
| 78 | 39, 77 | eqeltrid 2845 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) |
| 79 | | resttop 23168 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Top) |
| 80 | 38, 78, 79 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Top) |
| 81 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 82 | 81 | restin 23174 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = (𝐽 ↾t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽))) |
| 83 | 38, 78, 82 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = (𝐽 ↾t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽))) |
| 84 | 83 | unieqd 4920 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ (𝐽
↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ∪ (𝐽 ↾t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽))) |
| 85 | | inss2 4238 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝐽 |
| 86 | | fiuncmp.1 |
. . . . . . . . . . . . . 14
⊢ 𝑋 = ∪
𝐽 |
| 87 | 85, 86 | sseqtrri 4033 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) ⊆ 𝑋 |
| 88 | 86 | restuni 23170 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) ⊆ 𝑋) → (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ∪
(𝐽 ↾t
(∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽))) |
| 89 | 38, 87, 88 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ∪
(𝐽 ↾t
(∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽))) |
| 90 | 84, 89 | eqtr4d 2780 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ (𝐽
↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = (∪
𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)) |
| 91 | 52 | uneq2i 4165 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪
𝑥 ∈ {𝑧}𝐵) = (∪
𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵) |
| 92 | 39, 91 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 = (∪
𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵) |
| 93 | 92 | ineq1i 4216 |
. . . . . . . . . . . 12
⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵) ∩ ∪ 𝐽) |
| 94 | | indir 4286 |
. . . . . . . . . . . 12
⊢
((∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵) ∩ ∪ 𝐽) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) |
| 95 | 93, 94 | eqtri 2765 |
. . . . . . . . . . 11
⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) |
| 96 | 90, 95 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ (𝐽
↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ((∪
𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))) |
| 97 | | inss1 4237 |
. . . . . . . . . . . . . . 15
⊢ (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ 𝑦 𝐵 |
| 98 | | ssun1 4178 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪
𝑥 ∈ {𝑧}𝐵) |
| 99 | 98, 39 | sseqtrri 4033 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ∪
𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 |
| 100 | 97, 99 | sstri 3993 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 |
| 101 | 100 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) |
| 102 | | restabs 23173 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∧ ∪
𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽))) |
| 103 | 38, 101, 78, 102 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽))) |
| 104 | 81 | restin 23174 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V) → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) = (𝐽 ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽))) |
| 105 | 38, 44, 104 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) = (𝐽 ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽))) |
| 106 | 103, 105 | eqtr4d 2780 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵)) |
| 107 | 106, 40 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) ∈ Comp) |
| 108 | | inss1 4237 |
. . . . . . . . . . . . . . 15
⊢
(⦋𝑧 /
𝑥⦌𝐵 ∩ ∪ 𝐽)
⊆ ⦋𝑧 /
𝑥⦌𝐵 |
| 109 | | ssun2 4179 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑥 ∈ {𝑧}𝐵 ⊆ (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪
𝑥 ∈ {𝑧}𝐵) |
| 110 | 109, 39 | sseqtrri 4033 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑥 ∈ {𝑧}𝐵 ⊆ ∪
𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 |
| 111 | 52, 110 | eqsstrri 4031 |
. . . . . . . . . . . . . . 15
⊢
⦋𝑧 /
𝑥⦌𝐵 ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 |
| 112 | 108, 111 | sstri 3993 |
. . . . . . . . . . . . . 14
⊢
(⦋𝑧 /
𝑥⦌𝐵 ∩ ∪ 𝐽)
⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 |
| 113 | 112 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) |
| 114 | | restabs 23173 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧
(⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∧ ∪
𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))) |
| 115 | 38, 113, 78, 114 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))) |
| 116 | 81 | restin 23174 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧
⦋𝑧 / 𝑥⦌𝐵 ∈ V) → (𝐽 ↾t ⦋𝑧 / 𝑥⦌𝐵) = (𝐽 ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))) |
| 117 | 38, 74, 116 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾t ⦋𝑧 / 𝑥⦌𝐵) = (𝐽 ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))) |
| 118 | 115, 117 | eqtr4d 2780 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾t ⦋𝑧 / 𝑥⦌𝐵)) |
| 119 | 118, 70 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) ∈ Comp) |
| 120 | | eqid 2737 |
. . . . . . . . . . 11
⊢ ∪ (𝐽
↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ∪ (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) |
| 121 | 120 | uncmp 23411 |
. . . . . . . . . 10
⊢ ((((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Top ∧ ∪ (𝐽
↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ((∪
𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))) ∧ (((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) ∈ Comp ∧ ((𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) ∈ Comp)) → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp) |
| 122 | 80, 96, 107, 119, 121 | syl22anc 839 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp) |
| 123 | 122 | exp32 420 |
. . . . . . . 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 9204 |
. . 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) |