| Step | Hyp | Ref
| Expression |
| 1 | | ssel 3977 |
. . . . . . . . . . . . 13
⊢ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) →
(𝑤 ∈ 𝑦 → 𝑤 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪
{∅}))) |
| 2 | | elun 4153 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ↔
(𝑤 ∈ {𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∨ 𝑤 ∈ {∅})) |
| 3 | | sseq2 4010 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑤 → (𝑎 ⊆ 𝑧 ↔ 𝑎 ⊆ 𝑤)) |
| 4 | | pweq 4614 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑤 → 𝒫 𝑧 = 𝒫 𝑤) |
| 5 | 4 | ineq1d 4219 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑤 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑤 ∩ Fin)) |
| 6 | 5 | raleqdv 3326 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑤 → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 ↔ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪
𝑏)) |
| 7 | 3, 6 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑤 → ((𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ↔ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) |
| 8 | 7 | elrab 3692 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ↔ (𝑤 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) |
| 9 | | velsn 4642 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ {∅} ↔ 𝑤 = ∅) |
| 10 | 8, 9 | orbi12i 915 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∨ 𝑤 ∈ {∅}) ↔ ((𝑤 ∈ 𝒫
(fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) ∨ 𝑤 = ∅)) |
| 11 | 2, 10 | bitri 275 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ↔
((𝑤 ∈ 𝒫
(fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) ∨ 𝑤 = ∅)) |
| 12 | | elpwi 4607 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ 𝒫
(fi‘𝑥) → 𝑤 ⊆ (fi‘𝑥)) |
| 13 | 12 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ 𝒫
(fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) → 𝑤 ⊆ (fi‘𝑥)) |
| 14 | | 0ss 4400 |
. . . . . . . . . . . . . . . 16
⊢ ∅
⊆ (fi‘𝑥) |
| 15 | | sseq1 4009 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = ∅ → (𝑤 ⊆ (fi‘𝑥) ↔ ∅ ⊆
(fi‘𝑥))) |
| 16 | 14, 15 | mpbiri 258 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = ∅ → 𝑤 ⊆ (fi‘𝑥)) |
| 17 | 13, 16 | jaoi 858 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 ∈ 𝒫
(fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) ∨ 𝑤 = ∅) → 𝑤 ⊆ (fi‘𝑥)) |
| 18 | 11, 17 | sylbi 217 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) → 𝑤 ⊆ (fi‘𝑥)) |
| 19 | 1, 18 | syl6 35 |
. . . . . . . . . . . 12
⊢ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) →
(𝑤 ∈ 𝑦 → 𝑤 ⊆ (fi‘𝑥))) |
| 20 | 19 | ralrimiv 3145 |
. . . . . . . . . . 11
⊢ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) →
∀𝑤 ∈ 𝑦 𝑤 ⊆ (fi‘𝑥)) |
| 21 | | unissb 4939 |
. . . . . . . . . . 11
⊢ (∪ 𝑦
⊆ (fi‘𝑥) ↔
∀𝑤 ∈ 𝑦 𝑤 ⊆ (fi‘𝑥)) |
| 22 | 20, 21 | sylibr 234 |
. . . . . . . . . 10
⊢ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) → ∪ 𝑦
⊆ (fi‘𝑥)) |
| 23 | 22 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦)
→ ∪ 𝑦 ⊆ (fi‘𝑥)) |
| 24 | 23 | ad2antlr 727 |
. . . . . . . 8
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → ∪ 𝑦
⊆ (fi‘𝑥)) |
| 25 | | vuniex 7759 |
. . . . . . . . 9
⊢ ∪ 𝑦
∈ V |
| 26 | 25 | elpw 4604 |
. . . . . . . 8
⊢ (∪ 𝑦
∈ 𝒫 (fi‘𝑥) ↔ ∪ 𝑦 ⊆ (fi‘𝑥)) |
| 27 | 24, 26 | sylibr 234 |
. . . . . . 7
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → ∪ 𝑦
∈ 𝒫 (fi‘𝑥)) |
| 28 | | uni0b 4933 |
. . . . . . . . . 10
⊢ (∪ 𝑦 =
∅ ↔ 𝑦 ⊆
{∅}) |
| 29 | 28 | notbii 320 |
. . . . . . . . 9
⊢ (¬
∪ 𝑦 = ∅ ↔ ¬ 𝑦 ⊆ {∅}) |
| 30 | | disjssun 4468 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∩ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) = ∅ → (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ↔ 𝑦 ⊆
{∅})) |
| 31 | 30 | biimpcd 249 |
. . . . . . . . . . . 12
⊢ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) →
((𝑦 ∩ {𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) = ∅ → 𝑦 ⊆
{∅})) |
| 32 | 31 | necon3bd 2954 |
. . . . . . . . . . 11
⊢ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) →
(¬ 𝑦 ⊆ {∅}
→ (𝑦 ∩ {𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) ≠
∅)) |
| 33 | | n0 4353 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∩ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) ≠ ∅ ↔
∃𝑤 𝑤 ∈ (𝑦 ∩ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)})) |
| 34 | | elin 3967 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ (𝑦 ∩ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) ↔ (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)})) |
| 35 | 8 | anbi2i 623 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ 𝑦 ∧ 𝑤 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) ↔ (𝑤 ∈ 𝑦 ∧ (𝑤 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)))) |
| 36 | 34, 35 | bitri 275 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ (𝑦 ∩ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) ↔ (𝑤 ∈ 𝑦 ∧ (𝑤 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)))) |
| 37 | | simprrl 781 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ 𝑦 ∧ (𝑤 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → 𝑎 ⊆ 𝑤) |
| 38 | | simpl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ 𝑦 ∧ (𝑤 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → 𝑤 ∈ 𝑦) |
| 39 | | ssuni 4932 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ⊆ 𝑤 ∧ 𝑤 ∈ 𝑦) → 𝑎 ⊆ ∪ 𝑦) |
| 40 | 37, 38, 39 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ 𝑦 ∧ (𝑤 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → 𝑎 ⊆ ∪ 𝑦) |
| 41 | 36, 40 | sylbi 217 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (𝑦 ∩ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) → 𝑎 ⊆ ∪ 𝑦) |
| 42 | 41 | exlimiv 1930 |
. . . . . . . . . . . 12
⊢
(∃𝑤 𝑤 ∈ (𝑦 ∩ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) → 𝑎 ⊆ ∪ 𝑦) |
| 43 | 33, 42 | sylbi 217 |
. . . . . . . . . . 11
⊢ ((𝑦 ∩ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) ≠ ∅ → 𝑎 ⊆ ∪ 𝑦) |
| 44 | 32, 43 | syl6 35 |
. . . . . . . . . 10
⊢ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) →
(¬ 𝑦 ⊆ {∅}
→ 𝑎 ⊆ ∪ 𝑦)) |
| 45 | 44 | ad2antrl 728 |
. . . . . . . . 9
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
→ (¬ 𝑦 ⊆
{∅} → 𝑎 ⊆
∪ 𝑦)) |
| 46 | 29, 45 | biimtrid 242 |
. . . . . . . 8
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
→ (¬ ∪ 𝑦 = ∅ → 𝑎 ⊆ ∪ 𝑦)) |
| 47 | 46 | imp 406 |
. . . . . . 7
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → 𝑎 ⊆ ∪ 𝑦) |
| 48 | | elfpw 9394 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (𝒫 ∪ 𝑦
∩ Fin) ↔ (𝑛
⊆ ∪ 𝑦 ∧ 𝑛 ∈ Fin)) |
| 49 | | unieq 4918 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = ∅ → ∪ 𝑦 =
∪ ∅) |
| 50 | | uni0 4935 |
. . . . . . . . . . . . . . . . . . 19
⊢ ∪ ∅ = ∅ |
| 51 | 49, 50 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = ∅ → ∪ 𝑦 =
∅) |
| 52 | 51 | necon3bi 2967 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
∪ 𝑦 = ∅ → 𝑦 ≠ ∅) |
| 53 | 52 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((¬
∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin) → 𝑦 ≠ ∅) |
| 54 | 53 | ad2antrl 728 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ((¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin) ∧ 𝑛 ⊆ ∪ 𝑦)) → 𝑦 ≠ ∅) |
| 55 | | simplrr 778 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ((¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin) ∧ 𝑛 ⊆ ∪ 𝑦)) → [⊊] Or
𝑦) |
| 56 | | simprlr 780 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ((¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin) ∧ 𝑛 ⊆ ∪ 𝑦)) → 𝑛 ∈ Fin) |
| 57 | | simprr 773 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ((¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin) ∧ 𝑛 ⊆ ∪ 𝑦)) → 𝑛 ⊆ ∪ 𝑦) |
| 58 | | finsschain 9399 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ≠ ∅ ∧
[⊊] Or 𝑦)
∧ (𝑛 ∈ Fin ∧
𝑛 ⊆ ∪ 𝑦))
→ ∃𝑤 ∈
𝑦 𝑛 ⊆ 𝑤) |
| 59 | 54, 55, 56, 57, 58 | syl22anc 839 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ((¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin) ∧ 𝑛 ⊆ ∪ 𝑦)) → ∃𝑤 ∈ 𝑦 𝑛 ⊆ 𝑤) |
| 60 | 59 | expr 456 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ (¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin)) → (𝑛 ⊆ ∪ 𝑦 → ∃𝑤 ∈ 𝑦 𝑛 ⊆ 𝑤)) |
| 61 | | 0elpw 5356 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∅
∈ 𝒫 𝑎 |
| 62 | | 0fi 9082 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∅
∈ Fin |
| 63 | 61, 62 | elini 4199 |
. . . . . . . . . . . . . . . . . . 19
⊢ ∅
∈ (𝒫 𝑎 ∩
Fin) |
| 64 | | unieq 4918 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 = ∅ → ∪ 𝑏 =
∪ ∅) |
| 65 | 64 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 = ∅ → (𝑋 = ∪
𝑏 ↔ 𝑋 = ∪
∅)) |
| 66 | 65 | notbid 318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = ∅ → (¬ 𝑋 = ∪
𝑏 ↔ ¬ 𝑋 = ∪
∅)) |
| 67 | 66 | rspccv 3619 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑏 ∈
(𝒫 𝑎 ∩ Fin)
¬ 𝑋 = ∪ 𝑏
→ (∅ ∈ (𝒫 𝑎 ∩ Fin) → ¬ 𝑋 = ∪
∅)) |
| 68 | 63, 67 | mpi 20 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑏 ∈
(𝒫 𝑎 ∩ Fin)
¬ 𝑋 = ∪ 𝑏
→ ¬ 𝑋 = ∪ ∅) |
| 69 | | velpw 4605 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 ∈ 𝒫 𝑤 ↔ 𝑛 ⊆ 𝑤) |
| 70 | | elin 3967 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 ∈ (𝒫 𝑤 ∩ Fin) ↔ (𝑛 ∈ 𝒫 𝑤 ∧ 𝑛 ∈ Fin)) |
| 71 | | unieq 4918 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑏 = 𝑛 → ∪ 𝑏 = ∪
𝑛) |
| 72 | 71 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑏 = 𝑛 → (𝑋 = ∪ 𝑏 ↔ 𝑋 = ∪ 𝑛)) |
| 73 | 72 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑏 = 𝑛 → (¬ 𝑋 = ∪ 𝑏 ↔ ¬ 𝑋 = ∪ 𝑛)) |
| 74 | 73 | rspccv 3619 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∀𝑏 ∈
(𝒫 𝑤 ∩ Fin)
¬ 𝑋 = ∪ 𝑏
→ (𝑛 ∈ (𝒫
𝑤 ∩ Fin) → ¬
𝑋 = ∪ 𝑛)) |
| 75 | 70, 74 | biimtrrid 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∀𝑏 ∈
(𝒫 𝑤 ∩ Fin)
¬ 𝑋 = ∪ 𝑏
→ ((𝑛 ∈ 𝒫
𝑤 ∧ 𝑛 ∈ Fin) → ¬ 𝑋 = ∪ 𝑛)) |
| 76 | 75 | expd 415 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∀𝑏 ∈
(𝒫 𝑤 ∩ Fin)
¬ 𝑋 = ∪ 𝑏
→ (𝑛 ∈ 𝒫
𝑤 → (𝑛 ∈ Fin → ¬ 𝑋 = ∪
𝑛))) |
| 77 | 69, 76 | biimtrrid 243 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∀𝑏 ∈
(𝒫 𝑤 ∩ Fin)
¬ 𝑋 = ∪ 𝑏
→ (𝑛 ⊆ 𝑤 → (𝑛 ∈ Fin → ¬ 𝑋 = ∪ 𝑛))) |
| 78 | 77 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∀𝑏 ∈
(𝒫 𝑤 ∩ Fin)
¬ 𝑋 = ∪ 𝑏
→ (𝑛 ∈ Fin →
(𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛))) |
| 79 | 78 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑤 ∈ 𝒫
(fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) → (𝑛 ∈ Fin → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛))) |
| 80 | 79 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝑋 = ∪ ∅ → ((𝑤 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) → (𝑛 ∈ Fin → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛)))) |
| 81 | | sseq2 4010 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = ∅ → (𝑛 ⊆ 𝑤 ↔ 𝑛 ⊆ ∅)) |
| 82 | | ss0 4402 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 ⊆ ∅ → 𝑛 = ∅) |
| 83 | 81, 82 | biimtrdi 253 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = ∅ → (𝑛 ⊆ 𝑤 → 𝑛 = ∅)) |
| 84 | | unieq 4918 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 = ∅ → ∪ 𝑛 =
∪ ∅) |
| 85 | 84 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 = ∅ → (𝑋 = ∪
𝑛 ↔ 𝑋 = ∪
∅)) |
| 86 | 85 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 = ∅ → (¬ 𝑋 = ∪
𝑛 ↔ ¬ 𝑋 = ∪
∅)) |
| 87 | 86 | biimprcd 250 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
𝑋 = ∪ ∅ → (𝑛 = ∅ → ¬ 𝑋 = ∪ 𝑛)) |
| 88 | 87 | a1dd 50 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
𝑋 = ∪ ∅ → (𝑛 = ∅ → (𝑛 ∈ Fin → ¬ 𝑋 = ∪ 𝑛))) |
| 89 | 83, 88 | syl9r 78 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
𝑋 = ∪ ∅ → (𝑤 = ∅ → (𝑛 ⊆ 𝑤 → (𝑛 ∈ Fin → ¬ 𝑋 = ∪ 𝑛)))) |
| 90 | 89 | com34 91 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝑋 = ∪ ∅ → (𝑤 = ∅ → (𝑛 ∈ Fin → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛)))) |
| 91 | 80, 90 | jaod 860 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝑋 = ∪ ∅ → (((𝑤 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) ∨ 𝑤 = ∅) → (𝑛 ∈ Fin → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛)))) |
| 92 | 11, 91 | biimtrid 242 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑋 = ∪ ∅ → (𝑤 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) →
(𝑛 ∈ Fin → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛)))) |
| 93 | 1, 92 | sylan9r 508 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((¬
𝑋 = ∪ ∅ ∧ 𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})) →
(𝑤 ∈ 𝑦 → (𝑛 ∈ Fin → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛)))) |
| 94 | 93 | com23 86 |
. . . . . . . . . . . . . . . . . 18
⊢ ((¬
𝑋 = ∪ ∅ ∧ 𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})) →
(𝑛 ∈ Fin → (𝑤 ∈ 𝑦 → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛)))) |
| 95 | 68, 94 | sylan 580 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑏 ∈
(𝒫 𝑎 ∩ Fin)
¬ 𝑋 = ∪ 𝑏
∧ 𝑦 ⊆ ({𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})) →
(𝑛 ∈ Fin → (𝑤 ∈ 𝑦 → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛)))) |
| 96 | 95 | ad2ant2lr 748 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
→ (𝑛 ∈ Fin →
(𝑤 ∈ 𝑦 → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛)))) |
| 97 | 96 | imp 406 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ 𝑛 ∈ Fin) →
(𝑤 ∈ 𝑦 → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛))) |
| 98 | 97 | adantrl 716 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ (¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin)) → (𝑤 ∈ 𝑦 → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛))) |
| 99 | 98 | rexlimdv 3153 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ (¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin)) → (∃𝑤 ∈ 𝑦 𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛)) |
| 100 | 60, 99 | syld 47 |
. . . . . . . . . . . 12
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ (¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin)) → (𝑛 ⊆ ∪ 𝑦 → ¬ 𝑋 = ∪ 𝑛)) |
| 101 | 100 | expr 456 |
. . . . . . . . . . 11
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → (𝑛 ∈ Fin → (𝑛 ⊆ ∪ 𝑦 → ¬ 𝑋 = ∪ 𝑛))) |
| 102 | 101 | impcomd 411 |
. . . . . . . . . 10
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → ((𝑛 ⊆ ∪ 𝑦 ∧ 𝑛 ∈ Fin) → ¬ 𝑋 = ∪ 𝑛)) |
| 103 | 48, 102 | biimtrid 242 |
. . . . . . . . 9
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → (𝑛 ∈ (𝒫 ∪ 𝑦
∩ Fin) → ¬ 𝑋 =
∪ 𝑛)) |
| 104 | 103 | ralrimiv 3145 |
. . . . . . . 8
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → ∀𝑛 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑛) |
| 105 | | unieq 4918 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑏 → ∪ 𝑛 = ∪
𝑏) |
| 106 | 105 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑏 → (𝑋 = ∪ 𝑛 ↔ 𝑋 = ∪ 𝑏)) |
| 107 | 106 | notbid 318 |
. . . . . . . . 9
⊢ (𝑛 = 𝑏 → (¬ 𝑋 = ∪ 𝑛 ↔ ¬ 𝑋 = ∪ 𝑏)) |
| 108 | 107 | cbvralvw 3237 |
. . . . . . . 8
⊢
(∀𝑛 ∈
(𝒫 ∪ 𝑦 ∩ Fin) ¬ 𝑋 = ∪ 𝑛 ↔ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏) |
| 109 | 104, 108 | sylib 218 |
. . . . . . 7
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏) |
| 110 | 27, 47, 109 | jca32 515 |
. . . . . 6
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → (∪ 𝑦
∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏))) |
| 111 | 110 | ex 412 |
. . . . 5
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
→ (¬ ∪ 𝑦 = ∅ → (∪ 𝑦
∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏)))) |
| 112 | | orcom 871 |
. . . . . 6
⊢ ((∪ 𝑦
∈ {∅} ∨ ∪ 𝑦 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) ↔ (∪ 𝑦
∈ {𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∨ ∪ 𝑦
∈ {∅})) |
| 113 | 25 | elsn 4641 |
. . . . . . . 8
⊢ (∪ 𝑦
∈ {∅} ↔ ∪ 𝑦 = ∅) |
| 114 | | sseq2 4010 |
. . . . . . . . . 10
⊢ (𝑧 = ∪
𝑦 → (𝑎 ⊆ 𝑧 ↔ 𝑎 ⊆ ∪ 𝑦)) |
| 115 | | pweq 4614 |
. . . . . . . . . . . 12
⊢ (𝑧 = ∪
𝑦 → 𝒫 𝑧 = 𝒫 ∪ 𝑦) |
| 116 | 115 | ineq1d 4219 |
. . . . . . . . . . 11
⊢ (𝑧 = ∪
𝑦 → (𝒫 𝑧 ∩ Fin) = (𝒫 ∪ 𝑦
∩ Fin)) |
| 117 | 116 | raleqdv 3326 |
. . . . . . . . . 10
⊢ (𝑧 = ∪
𝑦 → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪
𝑏 ↔ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏)) |
| 118 | 114, 117 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑧 = ∪
𝑦 → ((𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ↔ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏))) |
| 119 | 118 | elrab 3692 |
. . . . . . . 8
⊢ (∪ 𝑦
∈ {𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ↔ (∪ 𝑦
∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏))) |
| 120 | 113, 119 | orbi12i 915 |
. . . . . . 7
⊢ ((∪ 𝑦
∈ {∅} ∨ ∪ 𝑦 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) ↔ (∪ 𝑦 =
∅ ∨ (∪ 𝑦 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏)))) |
| 121 | | df-or 849 |
. . . . . . 7
⊢ ((∪ 𝑦 =
∅ ∨ (∪ 𝑦 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
↔ (¬ ∪ 𝑦 = ∅ → (∪ 𝑦
∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏)))) |
| 122 | 120, 121 | bitr2i 276 |
. . . . . 6
⊢ ((¬
∪ 𝑦 = ∅ → (∪ 𝑦
∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
↔ (∪ 𝑦 ∈ {∅} ∨ ∪ 𝑦
∈ {𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)})) |
| 123 | | elun 4153 |
. . . . . 6
⊢ (∪ 𝑦
∈ ({𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ↔
(∪ 𝑦 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∨ ∪ 𝑦
∈ {∅})) |
| 124 | 112, 122,
123 | 3bitr4i 303 |
. . . . 5
⊢ ((¬
∪ 𝑦 = ∅ → (∪ 𝑦
∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
↔ ∪ 𝑦 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪
{∅})) |
| 125 | 111, 124 | sylib 218 |
. . . 4
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
→ ∪ 𝑦 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪
{∅})) |
| 126 | 125 | ex 412 |
. . 3
⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) → ((𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦)
→ ∪ 𝑦 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪
{∅}))) |
| 127 | 126 | alrimiv 1927 |
. 2
⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) → ∀𝑦((𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦)
→ ∪ 𝑦 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪
{∅}))) |
| 128 | | fvex 6919 |
. . . . . 6
⊢
(fi‘𝑥) ∈
V |
| 129 | 128 | pwex 5380 |
. . . . 5
⊢ 𝒫
(fi‘𝑥) ∈
V |
| 130 | 129 | rabex 5339 |
. . . 4
⊢ {𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∈ V |
| 131 | | p0ex 5384 |
. . . 4
⊢ {∅}
∈ V |
| 132 | 130, 131 | unex 7764 |
. . 3
⊢ ({𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∈
V |
| 133 | 132 | zorn 10547 |
. 2
⊢
(∀𝑦((𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦)
→ ∪ 𝑦 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})) →
∃𝑢 ∈ ({𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣) |
| 134 | 127, 133 | syl 17 |
1
⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) → ∃𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣) |