Step | Hyp | Ref
| Expression |
1 | | ssel 3562 |
. . . . . . . . . . . . 13
⊢ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) →
(𝑤 ∈ 𝑦 → 𝑤 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪
{∅}))) |
2 | | elun 3715 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ↔
(𝑤 ∈ {𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∨ 𝑤 ∈ {∅})) |
3 | | sseq2 3590 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑤 → (𝑎 ⊆ 𝑧 ↔ 𝑎 ⊆ 𝑤)) |
4 | | pweq 4111 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑤 → 𝒫 𝑧 = 𝒫 𝑤) |
5 | 4 | ineq1d 3775 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑤 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑤 ∩ Fin)) |
6 | 5 | raleqdv 3121 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑤 → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 ↔ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪
𝑏)) |
7 | 3, 6 | anbi12d 743 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑤 → ((𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ↔ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) |
8 | 7 | elrab 3331 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ↔ (𝑤 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) |
9 | | velsn 4141 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ {∅} ↔ 𝑤 = ∅) |
10 | 8, 9 | orbi12i 542 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∨ 𝑤 ∈ {∅}) ↔ ((𝑤 ∈ 𝒫
(fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) ∨ 𝑤 = ∅)) |
11 | 2, 10 | bitri 263 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ↔
((𝑤 ∈ 𝒫
(fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) ∨ 𝑤 = ∅)) |
12 | | elpwi 4117 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ 𝒫
(fi‘𝑥) → 𝑤 ⊆ (fi‘𝑥)) |
13 | 12 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ 𝒫
(fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) → 𝑤 ⊆ (fi‘𝑥)) |
14 | | 0ss 3924 |
. . . . . . . . . . . . . . . 16
⊢ ∅
⊆ (fi‘𝑥) |
15 | | sseq1 3589 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = ∅ → (𝑤 ⊆ (fi‘𝑥) ↔ ∅ ⊆
(fi‘𝑥))) |
16 | 14, 15 | mpbiri 247 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = ∅ → 𝑤 ⊆ (fi‘𝑥)) |
17 | 13, 16 | jaoi 393 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 ∈ 𝒫
(fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) ∨ 𝑤 = ∅) → 𝑤 ⊆ (fi‘𝑥)) |
18 | 11, 17 | sylbi 206 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) → 𝑤 ⊆ (fi‘𝑥)) |
19 | 1, 18 | syl6 34 |
. . . . . . . . . . . 12
⊢ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) →
(𝑤 ∈ 𝑦 → 𝑤 ⊆ (fi‘𝑥))) |
20 | 19 | ralrimiv 2948 |
. . . . . . . . . . 11
⊢ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) →
∀𝑤 ∈ 𝑦 𝑤 ⊆ (fi‘𝑥)) |
21 | | unissb 4405 |
. . . . . . . . . . 11
⊢ (∪ 𝑦
⊆ (fi‘𝑥) ↔
∀𝑤 ∈ 𝑦 𝑤 ⊆ (fi‘𝑥)) |
22 | 20, 21 | sylibr 223 |
. . . . . . . . . 10
⊢ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) → ∪ 𝑦
⊆ (fi‘𝑥)) |
23 | 22 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦)
→ ∪ 𝑦 ⊆ (fi‘𝑥)) |
24 | 23 | ad2antlr 759 |
. . . . . . . 8
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → ∪ 𝑦
⊆ (fi‘𝑥)) |
25 | | vuniex 6852 |
. . . . . . . . 9
⊢ ∪ 𝑦
∈ V |
26 | 25 | elpw 4114 |
. . . . . . . 8
⊢ (∪ 𝑦
∈ 𝒫 (fi‘𝑥) ↔ ∪ 𝑦 ⊆ (fi‘𝑥)) |
27 | 24, 26 | sylibr 223 |
. . . . . . 7
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → ∪ 𝑦
∈ 𝒫 (fi‘𝑥)) |
28 | | uni0b 4399 |
. . . . . . . . . 10
⊢ (∪ 𝑦 =
∅ ↔ 𝑦 ⊆
{∅}) |
29 | 28 | notbii 309 |
. . . . . . . . 9
⊢ (¬
∪ 𝑦 = ∅ ↔ ¬ 𝑦 ⊆ {∅}) |
30 | | disjssun 3988 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∩ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) = ∅ → (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ↔ 𝑦 ⊆
{∅})) |
31 | 30 | biimpcd 238 |
. . . . . . . . . . . 12
⊢ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) →
((𝑦 ∩ {𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) = ∅ → 𝑦 ⊆
{∅})) |
32 | 31 | necon3bd 2796 |
. . . . . . . . . . 11
⊢ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) →
(¬ 𝑦 ⊆ {∅}
→ (𝑦 ∩ {𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) ≠
∅)) |
33 | | n0 3890 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∩ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) ≠ ∅ ↔
∃𝑤 𝑤 ∈ (𝑦 ∩ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)})) |
34 | | elin 3758 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ (𝑦 ∩ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) ↔ (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)})) |
35 | 8 | anbi2i 726 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ 𝑦 ∧ 𝑤 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) ↔ (𝑤 ∈ 𝑦 ∧ (𝑤 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)))) |
36 | 34, 35 | bitri 263 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ (𝑦 ∩ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) ↔ (𝑤 ∈ 𝑦 ∧ (𝑤 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)))) |
37 | | simprrl 800 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ 𝑦 ∧ (𝑤 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → 𝑎 ⊆ 𝑤) |
38 | | simpl 472 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ 𝑦 ∧ (𝑤 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → 𝑤 ∈ 𝑦) |
39 | | ssuni 4395 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ⊆ 𝑤 ∧ 𝑤 ∈ 𝑦) → 𝑎 ⊆ ∪ 𝑦) |
40 | 37, 38, 39 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ 𝑦 ∧ (𝑤 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → 𝑎 ⊆ ∪ 𝑦) |
41 | 36, 40 | sylbi 206 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (𝑦 ∩ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) → 𝑎 ⊆ ∪ 𝑦) |
42 | 41 | exlimiv 1845 |
. . . . . . . . . . . 12
⊢
(∃𝑤 𝑤 ∈ (𝑦 ∩ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) → 𝑎 ⊆ ∪ 𝑦) |
43 | 33, 42 | sylbi 206 |
. . . . . . . . . . 11
⊢ ((𝑦 ∩ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) ≠ ∅ → 𝑎 ⊆ ∪ 𝑦) |
44 | 32, 43 | syl6 34 |
. . . . . . . . . 10
⊢ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) →
(¬ 𝑦 ⊆ {∅}
→ 𝑎 ⊆ ∪ 𝑦)) |
45 | 44 | ad2antrl 760 |
. . . . . . . . 9
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
→ (¬ 𝑦 ⊆
{∅} → 𝑎 ⊆
∪ 𝑦)) |
46 | 29, 45 | syl5bi 231 |
. . . . . . . 8
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
→ (¬ ∪ 𝑦 = ∅ → 𝑎 ⊆ ∪ 𝑦)) |
47 | 46 | imp 444 |
. . . . . . 7
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → 𝑎 ⊆ ∪ 𝑦) |
48 | | elfpw 8151 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (𝒫 ∪ 𝑦
∩ Fin) ↔ (𝑛
⊆ ∪ 𝑦 ∧ 𝑛 ∈ Fin)) |
49 | | unieq 4380 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = ∅ → ∪ 𝑦 =
∪ ∅) |
50 | | uni0 4401 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∪ ∅ = ∅ |
51 | 49, 50 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = ∅ → ∪ 𝑦 =
∅) |
52 | 51 | necon3bi 2808 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
∪ 𝑦 = ∅ → 𝑦 ≠ ∅) |
53 | 52 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((¬
∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin) → 𝑦 ≠ ∅) |
54 | 53 | ad2antrl 760 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ((¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin) ∧ 𝑛 ⊆ ∪ 𝑦)) → 𝑦 ≠ ∅) |
55 | | simplrr 797 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ((¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin) ∧ 𝑛 ⊆ ∪ 𝑦)) → [⊊] Or
𝑦) |
56 | | simprlr 799 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ((¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin) ∧ 𝑛 ⊆ ∪ 𝑦)) → 𝑛 ∈ Fin) |
57 | | simprr 792 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ((¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin) ∧ 𝑛 ⊆ ∪ 𝑦)) → 𝑛 ⊆ ∪ 𝑦) |
58 | | finsschain 8156 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ≠ ∅ ∧
[⊊] Or 𝑦)
∧ (𝑛 ∈ Fin ∧
𝑛 ⊆ ∪ 𝑦))
→ ∃𝑤 ∈
𝑦 𝑛 ⊆ 𝑤) |
59 | 54, 55, 56, 57, 58 | syl22anc 1319 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ((¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin) ∧ 𝑛 ⊆ ∪ 𝑦)) → ∃𝑤 ∈ 𝑦 𝑛 ⊆ 𝑤) |
60 | 59 | expr 641 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ (¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin)) → (𝑛 ⊆ ∪ 𝑦 → ∃𝑤 ∈ 𝑦 𝑛 ⊆ 𝑤)) |
61 | | 0elpw 4760 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ∅
∈ 𝒫 𝑎 |
62 | | 0fin 8073 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ∅
∈ Fin |
63 | | elin 3758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (∅
∈ (𝒫 𝑎 ∩
Fin) ↔ (∅ ∈ 𝒫 𝑎 ∧ ∅ ∈ Fin)) |
64 | 61, 62, 63 | mpbir2an 957 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∅
∈ (𝒫 𝑎 ∩
Fin) |
65 | | unieq 4380 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑏 = ∅ → ∪ 𝑏 =
∪ ∅) |
66 | 65 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 = ∅ → (𝑋 = ∪
𝑏 ↔ 𝑋 = ∪
∅)) |
67 | 66 | notbid 307 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 = ∅ → (¬ 𝑋 = ∪
𝑏 ↔ ¬ 𝑋 = ∪
∅)) |
68 | 67 | rspccv 3279 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑏 ∈
(𝒫 𝑎 ∩ Fin)
¬ 𝑋 = ∪ 𝑏
→ (∅ ∈ (𝒫 𝑎 ∩ Fin) → ¬ 𝑋 = ∪
∅)) |
69 | 64, 68 | mpi 20 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑏 ∈
(𝒫 𝑎 ∩ Fin)
¬ 𝑋 = ∪ 𝑏
→ ¬ 𝑋 = ∪ ∅) |
70 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 𝑛 ∈ V |
71 | 70 | elpw 4114 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 ∈ 𝒫 𝑤 ↔ 𝑛 ⊆ 𝑤) |
72 | | elin 3758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑛 ∈ (𝒫 𝑤 ∩ Fin) ↔ (𝑛 ∈ 𝒫 𝑤 ∧ 𝑛 ∈ Fin)) |
73 | | unieq 4380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑏 = 𝑛 → ∪ 𝑏 = ∪
𝑛) |
74 | 73 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑏 = 𝑛 → (𝑋 = ∪ 𝑏 ↔ 𝑋 = ∪ 𝑛)) |
75 | 74 | notbid 307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑏 = 𝑛 → (¬ 𝑋 = ∪ 𝑏 ↔ ¬ 𝑋 = ∪ 𝑛)) |
76 | 75 | rspccv 3279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(∀𝑏 ∈
(𝒫 𝑤 ∩ Fin)
¬ 𝑋 = ∪ 𝑏
→ (𝑛 ∈ (𝒫
𝑤 ∩ Fin) → ¬
𝑋 = ∪ 𝑛)) |
77 | 72, 76 | syl5bir 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∀𝑏 ∈
(𝒫 𝑤 ∩ Fin)
¬ 𝑋 = ∪ 𝑏
→ ((𝑛 ∈ 𝒫
𝑤 ∧ 𝑛 ∈ Fin) → ¬ 𝑋 = ∪ 𝑛)) |
78 | 77 | expd 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∀𝑏 ∈
(𝒫 𝑤 ∩ Fin)
¬ 𝑋 = ∪ 𝑏
→ (𝑛 ∈ 𝒫
𝑤 → (𝑛 ∈ Fin → ¬ 𝑋 = ∪
𝑛))) |
79 | 71, 78 | syl5bir 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∀𝑏 ∈
(𝒫 𝑤 ∩ Fin)
¬ 𝑋 = ∪ 𝑏
→ (𝑛 ⊆ 𝑤 → (𝑛 ∈ Fin → ¬ 𝑋 = ∪ 𝑛))) |
80 | 79 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∀𝑏 ∈
(𝒫 𝑤 ∩ Fin)
¬ 𝑋 = ∪ 𝑏
→ (𝑛 ∈ Fin →
(𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛))) |
81 | 80 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑤 ∈ 𝒫
(fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) → (𝑛 ∈ Fin → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛))) |
82 | 81 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
𝑋 = ∪ ∅ → ((𝑤 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) → (𝑛 ∈ Fin → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛)))) |
83 | | sseq2 3590 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 = ∅ → (𝑛 ⊆ 𝑤 ↔ 𝑛 ⊆ ∅)) |
84 | | ss0 3926 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 ⊆ ∅ → 𝑛 = ∅) |
85 | 83, 84 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = ∅ → (𝑛 ⊆ 𝑤 → 𝑛 = ∅)) |
86 | | unieq 4380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑛 = ∅ → ∪ 𝑛 =
∪ ∅) |
87 | 86 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 = ∅ → (𝑋 = ∪
𝑛 ↔ 𝑋 = ∪
∅)) |
88 | 87 | notbid 307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 = ∅ → (¬ 𝑋 = ∪
𝑛 ↔ ¬ 𝑋 = ∪
∅)) |
89 | 88 | biimprcd 239 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (¬
𝑋 = ∪ ∅ → (𝑛 = ∅ → ¬ 𝑋 = ∪ 𝑛)) |
90 | 89 | a1dd 48 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
𝑋 = ∪ ∅ → (𝑛 = ∅ → (𝑛 ∈ Fin → ¬ 𝑋 = ∪ 𝑛))) |
91 | 85, 90 | syl9r 76 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
𝑋 = ∪ ∅ → (𝑤 = ∅ → (𝑛 ⊆ 𝑤 → (𝑛 ∈ Fin → ¬ 𝑋 = ∪ 𝑛)))) |
92 | 91 | com34 89 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
𝑋 = ∪ ∅ → (𝑤 = ∅ → (𝑛 ∈ Fin → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛)))) |
93 | 82, 92 | jaod 394 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝑋 = ∪ ∅ → (((𝑤 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) ∨ 𝑤 = ∅) → (𝑛 ∈ Fin → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛)))) |
94 | 11, 93 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝑋 = ∪ ∅ → (𝑤 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) →
(𝑛 ∈ Fin → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛)))) |
95 | 1, 94 | sylan9r 688 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((¬
𝑋 = ∪ ∅ ∧ 𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})) →
(𝑤 ∈ 𝑦 → (𝑛 ∈ Fin → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛)))) |
96 | 95 | com23 84 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((¬
𝑋 = ∪ ∅ ∧ 𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})) →
(𝑛 ∈ Fin → (𝑤 ∈ 𝑦 → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛)))) |
97 | 69, 96 | sylan 487 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑏 ∈
(𝒫 𝑎 ∩ Fin)
¬ 𝑋 = ∪ 𝑏
∧ 𝑦 ⊆ ({𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})) →
(𝑛 ∈ Fin → (𝑤 ∈ 𝑦 → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛)))) |
98 | 97 | ad2ant2lr 780 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
→ (𝑛 ∈ Fin →
(𝑤 ∈ 𝑦 → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛)))) |
99 | 98 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ 𝑛 ∈ Fin) →
(𝑤 ∈ 𝑦 → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛))) |
100 | 99 | adantrl 748 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ (¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin)) → (𝑤 ∈ 𝑦 → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛))) |
101 | 100 | rexlimdv 3012 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ (¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin)) → (∃𝑤 ∈ 𝑦 𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛)) |
102 | 60, 101 | syld 46 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ (¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin)) → (𝑛 ⊆ ∪ 𝑦 → ¬ 𝑋 = ∪ 𝑛)) |
103 | 102 | expr 641 |
. . . . . . . . . . . 12
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → (𝑛 ∈ Fin → (𝑛 ⊆ ∪ 𝑦 → ¬ 𝑋 = ∪ 𝑛))) |
104 | 103 | com23 84 |
. . . . . . . . . . 11
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → (𝑛 ⊆ ∪ 𝑦 → (𝑛 ∈ Fin → ¬ 𝑋 = ∪ 𝑛))) |
105 | 104 | impd 446 |
. . . . . . . . . 10
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → ((𝑛 ⊆ ∪ 𝑦 ∧ 𝑛 ∈ Fin) → ¬ 𝑋 = ∪ 𝑛)) |
106 | 48, 105 | syl5bi 231 |
. . . . . . . . 9
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → (𝑛 ∈ (𝒫 ∪ 𝑦
∩ Fin) → ¬ 𝑋 =
∪ 𝑛)) |
107 | 106 | ralrimiv 2948 |
. . . . . . . 8
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → ∀𝑛 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑛) |
108 | | unieq 4380 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑏 → ∪ 𝑛 = ∪
𝑏) |
109 | 108 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑏 → (𝑋 = ∪ 𝑛 ↔ 𝑋 = ∪ 𝑏)) |
110 | 109 | notbid 307 |
. . . . . . . . 9
⊢ (𝑛 = 𝑏 → (¬ 𝑋 = ∪ 𝑛 ↔ ¬ 𝑋 = ∪ 𝑏)) |
111 | 110 | cbvralv 3147 |
. . . . . . . 8
⊢
(∀𝑛 ∈
(𝒫 ∪ 𝑦 ∩ Fin) ¬ 𝑋 = ∪ 𝑛 ↔ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏) |
112 | 107, 111 | sylib 207 |
. . . . . . 7
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏) |
113 | 27, 47, 112 | jca32 556 |
. . . . . 6
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → (∪ 𝑦
∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏))) |
114 | 113 | ex 449 |
. . . . 5
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
→ (¬ ∪ 𝑦 = ∅ → (∪ 𝑦
∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏)))) |
115 | | orcom 401 |
. . . . . 6
⊢ ((∪ 𝑦
∈ {∅} ∨ ∪ 𝑦 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) ↔ (∪ 𝑦
∈ {𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∨ ∪ 𝑦
∈ {∅})) |
116 | 25 | elsn 4140 |
. . . . . . . 8
⊢ (∪ 𝑦
∈ {∅} ↔ ∪ 𝑦 = ∅) |
117 | | sseq2 3590 |
. . . . . . . . . 10
⊢ (𝑧 = ∪
𝑦 → (𝑎 ⊆ 𝑧 ↔ 𝑎 ⊆ ∪ 𝑦)) |
118 | | pweq 4111 |
. . . . . . . . . . . 12
⊢ (𝑧 = ∪
𝑦 → 𝒫 𝑧 = 𝒫 ∪ 𝑦) |
119 | 118 | ineq1d 3775 |
. . . . . . . . . . 11
⊢ (𝑧 = ∪
𝑦 → (𝒫 𝑧 ∩ Fin) = (𝒫 ∪ 𝑦
∩ Fin)) |
120 | 119 | raleqdv 3121 |
. . . . . . . . . 10
⊢ (𝑧 = ∪
𝑦 → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪
𝑏 ↔ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏)) |
121 | 117, 120 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑧 = ∪
𝑦 → ((𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ↔ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏))) |
122 | 121 | elrab 3331 |
. . . . . . . 8
⊢ (∪ 𝑦
∈ {𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ↔ (∪ 𝑦
∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏))) |
123 | 116, 122 | orbi12i 542 |
. . . . . . 7
⊢ ((∪ 𝑦
∈ {∅} ∨ ∪ 𝑦 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) ↔ (∪ 𝑦 =
∅ ∨ (∪ 𝑦 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏)))) |
124 | | df-or 384 |
. . . . . . 7
⊢ ((∪ 𝑦 =
∅ ∨ (∪ 𝑦 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
↔ (¬ ∪ 𝑦 = ∅ → (∪ 𝑦
∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏)))) |
125 | 123, 124 | bitr2i 264 |
. . . . . 6
⊢ ((¬
∪ 𝑦 = ∅ → (∪ 𝑦
∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
↔ (∪ 𝑦 ∈ {∅} ∨ ∪ 𝑦
∈ {𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)})) |
126 | | elun 3715 |
. . . . . 6
⊢ (∪ 𝑦
∈ ({𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ↔
(∪ 𝑦 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∨ ∪ 𝑦
∈ {∅})) |
127 | 115, 125,
126 | 3bitr4i 291 |
. . . . 5
⊢ ((¬
∪ 𝑦 = ∅ → (∪ 𝑦
∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
↔ ∪ 𝑦 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪
{∅})) |
128 | 114, 127 | sylib 207 |
. . . 4
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
→ ∪ 𝑦 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪
{∅})) |
129 | 128 | ex 449 |
. . 3
⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) → ((𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦)
→ ∪ 𝑦 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪
{∅}))) |
130 | 129 | alrimiv 1842 |
. 2
⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) → ∀𝑦((𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦)
→ ∪ 𝑦 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪
{∅}))) |
131 | | fvex 6113 |
. . . . . 6
⊢
(fi‘𝑥) ∈
V |
132 | 131 | pwex 4774 |
. . . . 5
⊢ 𝒫
(fi‘𝑥) ∈
V |
133 | 132 | rabex 4740 |
. . . 4
⊢ {𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∈ V |
134 | | p0ex 4779 |
. . . 4
⊢ {∅}
∈ V |
135 | 133, 134 | unex 6854 |
. . 3
⊢ ({𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∈
V |
136 | 135 | zorn 9212 |
. 2
⊢
(∀𝑦((𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦)
→ ∪ 𝑦 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})) →
∃𝑢 ∈ ({𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣) |
137 | 130, 136 | syl 17 |
1
⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) → ∃𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣) |