Step | Hyp | Ref
| Expression |
1 | | ssel 3919 |
. . . . . . . . . . . . 13
⊢ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) →
(𝑤 ∈ 𝑦 → 𝑤 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪
{∅}))) |
2 | | elun 4088 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ↔
(𝑤 ∈ {𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∨ 𝑤 ∈ {∅})) |
3 | | sseq2 3952 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑤 → (𝑎 ⊆ 𝑧 ↔ 𝑎 ⊆ 𝑤)) |
4 | | pweq 4555 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑤 → 𝒫 𝑧 = 𝒫 𝑤) |
5 | 4 | ineq1d 4151 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑤 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑤 ∩ Fin)) |
6 | 5 | raleqdv 3347 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑤 → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 ↔ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪
𝑏)) |
7 | 3, 6 | anbi12d 631 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑤 → ((𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ↔ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) |
8 | 7 | elrab 3626 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ↔ (𝑤 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) |
9 | | velsn 4583 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ {∅} ↔ 𝑤 = ∅) |
10 | 8, 9 | orbi12i 912 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∨ 𝑤 ∈ {∅}) ↔ ((𝑤 ∈ 𝒫
(fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) ∨ 𝑤 = ∅)) |
11 | 2, 10 | bitri 274 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ↔
((𝑤 ∈ 𝒫
(fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) ∨ 𝑤 = ∅)) |
12 | | elpwi 4548 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ 𝒫
(fi‘𝑥) → 𝑤 ⊆ (fi‘𝑥)) |
13 | 12 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ 𝒫
(fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) → 𝑤 ⊆ (fi‘𝑥)) |
14 | | 0ss 4336 |
. . . . . . . . . . . . . . . 16
⊢ ∅
⊆ (fi‘𝑥) |
15 | | sseq1 3951 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = ∅ → (𝑤 ⊆ (fi‘𝑥) ↔ ∅ ⊆
(fi‘𝑥))) |
16 | 14, 15 | mpbiri 257 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = ∅ → 𝑤 ⊆ (fi‘𝑥)) |
17 | 13, 16 | jaoi 854 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 ∈ 𝒫
(fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) ∨ 𝑤 = ∅) → 𝑤 ⊆ (fi‘𝑥)) |
18 | 11, 17 | sylbi 216 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) → 𝑤 ⊆ (fi‘𝑥)) |
19 | 1, 18 | syl6 35 |
. . . . . . . . . . . 12
⊢ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) →
(𝑤 ∈ 𝑦 → 𝑤 ⊆ (fi‘𝑥))) |
20 | 19 | ralrimiv 3109 |
. . . . . . . . . . 11
⊢ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) →
∀𝑤 ∈ 𝑦 𝑤 ⊆ (fi‘𝑥)) |
21 | | unissb 4879 |
. . . . . . . . . . 11
⊢ (∪ 𝑦
⊆ (fi‘𝑥) ↔
∀𝑤 ∈ 𝑦 𝑤 ⊆ (fi‘𝑥)) |
22 | 20, 21 | sylibr 233 |
. . . . . . . . . 10
⊢ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) → ∪ 𝑦
⊆ (fi‘𝑥)) |
23 | 22 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦)
→ ∪ 𝑦 ⊆ (fi‘𝑥)) |
24 | 23 | ad2antlr 724 |
. . . . . . . 8
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → ∪ 𝑦
⊆ (fi‘𝑥)) |
25 | | vuniex 7584 |
. . . . . . . . 9
⊢ ∪ 𝑦
∈ V |
26 | 25 | elpw 4543 |
. . . . . . . 8
⊢ (∪ 𝑦
∈ 𝒫 (fi‘𝑥) ↔ ∪ 𝑦 ⊆ (fi‘𝑥)) |
27 | 24, 26 | sylibr 233 |
. . . . . . 7
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → ∪ 𝑦
∈ 𝒫 (fi‘𝑥)) |
28 | | uni0b 4873 |
. . . . . . . . . 10
⊢ (∪ 𝑦 =
∅ ↔ 𝑦 ⊆
{∅}) |
29 | 28 | notbii 320 |
. . . . . . . . 9
⊢ (¬
∪ 𝑦 = ∅ ↔ ¬ 𝑦 ⊆ {∅}) |
30 | | disjssun 4407 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∩ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) = ∅ → (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ↔ 𝑦 ⊆
{∅})) |
31 | 30 | biimpcd 248 |
. . . . . . . . . . . 12
⊢ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) →
((𝑦 ∩ {𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) = ∅ → 𝑦 ⊆
{∅})) |
32 | 31 | necon3bd 2959 |
. . . . . . . . . . 11
⊢ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) →
(¬ 𝑦 ⊆ {∅}
→ (𝑦 ∩ {𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) ≠
∅)) |
33 | | n0 4286 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∩ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) ≠ ∅ ↔
∃𝑤 𝑤 ∈ (𝑦 ∩ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)})) |
34 | | elin 3908 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ (𝑦 ∩ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) ↔ (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)})) |
35 | 8 | anbi2i 623 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ 𝑦 ∧ 𝑤 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) ↔ (𝑤 ∈ 𝑦 ∧ (𝑤 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)))) |
36 | 34, 35 | bitri 274 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ (𝑦 ∩ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) ↔ (𝑤 ∈ 𝑦 ∧ (𝑤 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)))) |
37 | | simprrl 778 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ 𝑦 ∧ (𝑤 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → 𝑎 ⊆ 𝑤) |
38 | | simpl 483 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ 𝑦 ∧ (𝑤 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → 𝑤 ∈ 𝑦) |
39 | | ssuni 4872 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ⊆ 𝑤 ∧ 𝑤 ∈ 𝑦) → 𝑎 ⊆ ∪ 𝑦) |
40 | 37, 38, 39 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ 𝑦 ∧ (𝑤 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → 𝑎 ⊆ ∪ 𝑦) |
41 | 36, 40 | sylbi 216 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (𝑦 ∩ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) → 𝑎 ⊆ ∪ 𝑦) |
42 | 41 | exlimiv 1937 |
. . . . . . . . . . . 12
⊢
(∃𝑤 𝑤 ∈ (𝑦 ∩ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) → 𝑎 ⊆ ∪ 𝑦) |
43 | 33, 42 | sylbi 216 |
. . . . . . . . . . 11
⊢ ((𝑦 ∩ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) ≠ ∅ → 𝑎 ⊆ ∪ 𝑦) |
44 | 32, 43 | syl6 35 |
. . . . . . . . . 10
⊢ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) →
(¬ 𝑦 ⊆ {∅}
→ 𝑎 ⊆ ∪ 𝑦)) |
45 | 44 | ad2antrl 725 |
. . . . . . . . 9
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
→ (¬ 𝑦 ⊆
{∅} → 𝑎 ⊆
∪ 𝑦)) |
46 | 29, 45 | syl5bi 241 |
. . . . . . . 8
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
→ (¬ ∪ 𝑦 = ∅ → 𝑎 ⊆ ∪ 𝑦)) |
47 | 46 | imp 407 |
. . . . . . 7
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → 𝑎 ⊆ ∪ 𝑦) |
48 | | elfpw 9097 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (𝒫 ∪ 𝑦
∩ Fin) ↔ (𝑛
⊆ ∪ 𝑦 ∧ 𝑛 ∈ Fin)) |
49 | | unieq 4856 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = ∅ → ∪ 𝑦 =
∪ ∅) |
50 | | uni0 4875 |
. . . . . . . . . . . . . . . . . . 19
⊢ ∪ ∅ = ∅ |
51 | 49, 50 | eqtrdi 2796 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = ∅ → ∪ 𝑦 =
∅) |
52 | 51 | necon3bi 2972 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
∪ 𝑦 = ∅ → 𝑦 ≠ ∅) |
53 | 52 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((¬
∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin) → 𝑦 ≠ ∅) |
54 | 53 | ad2antrl 725 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ((¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin) ∧ 𝑛 ⊆ ∪ 𝑦)) → 𝑦 ≠ ∅) |
55 | | simplrr 775 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ((¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin) ∧ 𝑛 ⊆ ∪ 𝑦)) → [⊊] Or
𝑦) |
56 | | simprlr 777 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ((¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin) ∧ 𝑛 ⊆ ∪ 𝑦)) → 𝑛 ∈ Fin) |
57 | | simprr 770 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ((¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin) ∧ 𝑛 ⊆ ∪ 𝑦)) → 𝑛 ⊆ ∪ 𝑦) |
58 | | finsschain 9102 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ≠ ∅ ∧
[⊊] Or 𝑦)
∧ (𝑛 ∈ Fin ∧
𝑛 ⊆ ∪ 𝑦))
→ ∃𝑤 ∈
𝑦 𝑛 ⊆ 𝑤) |
59 | 54, 55, 56, 57, 58 | syl22anc 836 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ((¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin) ∧ 𝑛 ⊆ ∪ 𝑦)) → ∃𝑤 ∈ 𝑦 𝑛 ⊆ 𝑤) |
60 | 59 | expr 457 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ (¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin)) → (𝑛 ⊆ ∪ 𝑦 → ∃𝑤 ∈ 𝑦 𝑛 ⊆ 𝑤)) |
61 | | 0elpw 5282 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∅
∈ 𝒫 𝑎 |
62 | | 0fin 8934 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∅
∈ Fin |
63 | 61, 62 | elini 4132 |
. . . . . . . . . . . . . . . . . . 19
⊢ ∅
∈ (𝒫 𝑎 ∩
Fin) |
64 | | unieq 4856 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 = ∅ → ∪ 𝑏 =
∪ ∅) |
65 | 64 | eqeq2d 2751 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 = ∅ → (𝑋 = ∪
𝑏 ↔ 𝑋 = ∪
∅)) |
66 | 65 | notbid 318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = ∅ → (¬ 𝑋 = ∪
𝑏 ↔ ¬ 𝑋 = ∪
∅)) |
67 | 66 | rspccv 3558 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑏 ∈
(𝒫 𝑎 ∩ Fin)
¬ 𝑋 = ∪ 𝑏
→ (∅ ∈ (𝒫 𝑎 ∩ Fin) → ¬ 𝑋 = ∪
∅)) |
68 | 63, 67 | mpi 20 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑏 ∈
(𝒫 𝑎 ∩ Fin)
¬ 𝑋 = ∪ 𝑏
→ ¬ 𝑋 = ∪ ∅) |
69 | | velpw 4544 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 ∈ 𝒫 𝑤 ↔ 𝑛 ⊆ 𝑤) |
70 | | elin 3908 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 ∈ (𝒫 𝑤 ∩ Fin) ↔ (𝑛 ∈ 𝒫 𝑤 ∧ 𝑛 ∈ Fin)) |
71 | | unieq 4856 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑏 = 𝑛 → ∪ 𝑏 = ∪
𝑛) |
72 | 71 | eqeq2d 2751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑏 = 𝑛 → (𝑋 = ∪ 𝑏 ↔ 𝑋 = ∪ 𝑛)) |
73 | 72 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑏 = 𝑛 → (¬ 𝑋 = ∪ 𝑏 ↔ ¬ 𝑋 = ∪ 𝑛)) |
74 | 73 | rspccv 3558 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∀𝑏 ∈
(𝒫 𝑤 ∩ Fin)
¬ 𝑋 = ∪ 𝑏
→ (𝑛 ∈ (𝒫
𝑤 ∩ Fin) → ¬
𝑋 = ∪ 𝑛)) |
75 | 70, 74 | syl5bir 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∀𝑏 ∈
(𝒫 𝑤 ∩ Fin)
¬ 𝑋 = ∪ 𝑏
→ ((𝑛 ∈ 𝒫
𝑤 ∧ 𝑛 ∈ Fin) → ¬ 𝑋 = ∪ 𝑛)) |
76 | 75 | expd 416 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∀𝑏 ∈
(𝒫 𝑤 ∩ Fin)
¬ 𝑋 = ∪ 𝑏
→ (𝑛 ∈ 𝒫
𝑤 → (𝑛 ∈ Fin → ¬ 𝑋 = ∪
𝑛))) |
77 | 69, 76 | syl5bir 242 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∀𝑏 ∈
(𝒫 𝑤 ∩ Fin)
¬ 𝑋 = ∪ 𝑏
→ (𝑛 ⊆ 𝑤 → (𝑛 ∈ Fin → ¬ 𝑋 = ∪ 𝑛))) |
78 | 77 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∀𝑏 ∈
(𝒫 𝑤 ∩ Fin)
¬ 𝑋 = ∪ 𝑏
→ (𝑛 ∈ Fin →
(𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛))) |
79 | 78 | ad2antll 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑤 ∈ 𝒫
(fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) → (𝑛 ∈ Fin → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛))) |
80 | 79 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝑋 = ∪ ∅ → ((𝑤 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) → (𝑛 ∈ Fin → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛)))) |
81 | | sseq2 3952 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = ∅ → (𝑛 ⊆ 𝑤 ↔ 𝑛 ⊆ ∅)) |
82 | | ss0 4338 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 ⊆ ∅ → 𝑛 = ∅) |
83 | 81, 82 | syl6bi 252 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = ∅ → (𝑛 ⊆ 𝑤 → 𝑛 = ∅)) |
84 | | unieq 4856 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 = ∅ → ∪ 𝑛 =
∪ ∅) |
85 | 84 | eqeq2d 2751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 = ∅ → (𝑋 = ∪
𝑛 ↔ 𝑋 = ∪
∅)) |
86 | 85 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 = ∅ → (¬ 𝑋 = ∪
𝑛 ↔ ¬ 𝑋 = ∪
∅)) |
87 | 86 | biimprcd 249 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
𝑋 = ∪ ∅ → (𝑛 = ∅ → ¬ 𝑋 = ∪ 𝑛)) |
88 | 87 | a1dd 50 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
𝑋 = ∪ ∅ → (𝑛 = ∅ → (𝑛 ∈ Fin → ¬ 𝑋 = ∪ 𝑛))) |
89 | 83, 88 | syl9r 78 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
𝑋 = ∪ ∅ → (𝑤 = ∅ → (𝑛 ⊆ 𝑤 → (𝑛 ∈ Fin → ¬ 𝑋 = ∪ 𝑛)))) |
90 | 89 | com34 91 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝑋 = ∪ ∅ → (𝑤 = ∅ → (𝑛 ∈ Fin → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛)))) |
91 | 80, 90 | jaod 856 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝑋 = ∪ ∅ → (((𝑤 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑤 ∧ ∀𝑏 ∈ (𝒫 𝑤 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) ∨ 𝑤 = ∅) → (𝑛 ∈ Fin → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛)))) |
92 | 11, 91 | syl5bi 241 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑋 = ∪ ∅ → (𝑤 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) →
(𝑛 ∈ Fin → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛)))) |
93 | 1, 92 | sylan9r 509 |
. . . . . . . . . . . . . . . . . . 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 745 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
→ (𝑛 ∈ Fin →
(𝑤 ∈ 𝑦 → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛)))) |
97 | 96 | imp 407 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ 𝑛 ∈ Fin) →
(𝑤 ∈ 𝑦 → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛))) |
98 | 97 | adantrl 713 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ (¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin)) → (𝑤 ∈ 𝑦 → (𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛))) |
99 | 98 | rexlimdv 3214 |
. . . . . . . . . . . . 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 457 |
. . . . . . . . . . 11
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → (𝑛 ∈ Fin → (𝑛 ⊆ ∪ 𝑦 → ¬ 𝑋 = ∪ 𝑛))) |
102 | 101 | impcomd 412 |
. . . . . . . . . 10
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → ((𝑛 ⊆ ∪ 𝑦 ∧ 𝑛 ∈ Fin) → ¬ 𝑋 = ∪ 𝑛)) |
103 | 48, 102 | syl5bi 241 |
. . . . . . . . 9
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → (𝑛 ∈ (𝒫 ∪ 𝑦
∩ Fin) → ¬ 𝑋 =
∪ 𝑛)) |
104 | 103 | ralrimiv 3109 |
. . . . . . . 8
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → ∀𝑛 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑛) |
105 | | unieq 4856 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑏 → ∪ 𝑛 = ∪
𝑏) |
106 | 105 | eqeq2d 2751 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑏 → (𝑋 = ∪ 𝑛 ↔ 𝑋 = ∪ 𝑏)) |
107 | 106 | notbid 318 |
. . . . . . . . 9
⊢ (𝑛 = 𝑏 → (¬ 𝑋 = ∪ 𝑛 ↔ ¬ 𝑋 = ∪ 𝑏)) |
108 | 107 | cbvralvw 3381 |
. . . . . . . 8
⊢
(∀𝑛 ∈
(𝒫 ∪ 𝑦 ∩ Fin) ¬ 𝑋 = ∪ 𝑛 ↔ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏) |
109 | 104, 108 | sylib 217 |
. . . . . . 7
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏) |
110 | 27, 47, 109 | jca32 516 |
. . . . . 6
⊢
(((((𝐽 =
(topGen‘(fi‘𝑥))
∧ ∀𝑐 ∈
𝒫 𝑥(𝑋 = ∪
𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
∧ ¬ ∪ 𝑦 = ∅) → (∪ 𝑦
∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏))) |
111 | 110 | ex 413 |
. . . . 5
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
→ (¬ ∪ 𝑦 = ∅ → (∪ 𝑦
∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏)))) |
112 | | orcom 867 |
. . . . . 6
⊢ ((∪ 𝑦
∈ {∅} ∨ ∪ 𝑦 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) ↔ (∪ 𝑦
∈ {𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∨ ∪ 𝑦
∈ {∅})) |
113 | 25 | elsn 4582 |
. . . . . . . 8
⊢ (∪ 𝑦
∈ {∅} ↔ ∪ 𝑦 = ∅) |
114 | | sseq2 3952 |
. . . . . . . . . 10
⊢ (𝑧 = ∪
𝑦 → (𝑎 ⊆ 𝑧 ↔ 𝑎 ⊆ ∪ 𝑦)) |
115 | | pweq 4555 |
. . . . . . . . . . . 12
⊢ (𝑧 = ∪
𝑦 → 𝒫 𝑧 = 𝒫 ∪ 𝑦) |
116 | 115 | ineq1d 4151 |
. . . . . . . . . . 11
⊢ (𝑧 = ∪
𝑦 → (𝒫 𝑧 ∩ Fin) = (𝒫 ∪ 𝑦
∩ Fin)) |
117 | 116 | raleqdv 3347 |
. . . . . . . . . 10
⊢ (𝑧 = ∪
𝑦 → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪
𝑏 ↔ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏)) |
118 | 114, 117 | anbi12d 631 |
. . . . . . . . 9
⊢ (𝑧 = ∪
𝑦 → ((𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ↔ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏))) |
119 | 118 | elrab 3626 |
. . . . . . . 8
⊢ (∪ 𝑦
∈ {𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ↔ (∪ 𝑦
∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏))) |
120 | 113, 119 | orbi12i 912 |
. . . . . . 7
⊢ ((∪ 𝑦
∈ {∅} ∨ ∪ 𝑦 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)}) ↔ (∪ 𝑦 =
∅ ∨ (∪ 𝑦 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏)))) |
121 | | df-or 845 |
. . . . . . 7
⊢ ((∪ 𝑦 =
∅ ∨ (∪ 𝑦 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
↔ (¬ ∪ 𝑦 = ∅ → (∪ 𝑦
∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏)))) |
122 | 120, 121 | bitr2i 275 |
. . . . . 6
⊢ ((¬
∪ 𝑦 = ∅ → (∪ 𝑦
∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
↔ (∪ 𝑦 ∈ {∅} ∨ ∪ 𝑦
∈ {𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)})) |
123 | | elun 4088 |
. . . . . 6
⊢ (∪ 𝑦
∈ ({𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ↔
(∪ 𝑦 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∨ ∪ 𝑦
∈ {∅})) |
124 | 112, 122,
123 | 3bitr4i 303 |
. . . . 5
⊢ ((¬
∪ 𝑦 = ∅ → (∪ 𝑦
∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ ∪ 𝑦 ∧ ∀𝑏 ∈ (𝒫 ∪ 𝑦
∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
↔ ∪ 𝑦 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪
{∅})) |
125 | 111, 124 | sylib 217 |
. . . 4
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) ∧ (𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦))
→ ∪ 𝑦 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪
{∅})) |
126 | 125 | ex 413 |
. . 3
⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) → ((𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦)
→ ∪ 𝑦 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪
{∅}))) |
127 | 126 | alrimiv 1934 |
. 2
⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪
𝑏) → ∀𝑦((𝑦 ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧
[⊊] Or 𝑦)
→ ∪ 𝑦 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪
{∅}))) |
128 | | fvex 6782 |
. . . . . 6
⊢
(fi‘𝑥) ∈
V |
129 | 128 | pwex 5307 |
. . . . 5
⊢ 𝒫
(fi‘𝑥) ∈
V |
130 | 129 | rabex 5260 |
. . . 4
⊢ {𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∈ V |
131 | | p0ex 5311 |
. . . 4
⊢ {∅}
∈ V |
132 | 130, 131 | unex 7588 |
. . 3
⊢ ({𝑧 ∈ 𝒫
(fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∈
V |
133 | 132 | zorn 10262 |
. 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) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣) |