Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . 4
⊢ ∪ (𝐽
↾t 𝑆) =
∪ (𝐽 ↾t 𝑆) |
2 | 1 | iscmp 22309 |
. . 3
⊢ ((𝐽 ↾t 𝑆) ∈ Comp ↔ ((𝐽 ↾t 𝑆) ∈ Top ∧ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪
(𝐽 ↾t
𝑆) = ∪ 𝑠
→ ∃𝑡 ∈
(𝒫 𝑠 ∩
Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))) |
3 | | id 22 |
. . . . . 6
⊢ (𝑆 ⊆ 𝑋 → 𝑆 ⊆ 𝑋) |
4 | | cmpsub.1 |
. . . . . . 7
⊢ 𝑋 = ∪
𝐽 |
5 | 4 | topopn 21827 |
. . . . . 6
⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) |
6 | | ssexg 5230 |
. . . . . 6
⊢ ((𝑆 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽) → 𝑆 ∈ V) |
7 | 3, 5, 6 | syl2anr 600 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ∈ V) |
8 | | resttop 22081 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝐽 ↾t 𝑆) ∈ Top) |
9 | 7, 8 | syldan 594 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝐽 ↾t 𝑆) ∈ Top) |
10 | | ibar 532 |
. . . . 5
⊢ ((𝐽 ↾t 𝑆) ∈ Top →
(∀𝑠 ∈ 𝒫
(𝐽 ↾t
𝑆)(∪ (𝐽
↾t 𝑆) =
∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡)
↔ ((𝐽
↾t 𝑆)
∈ Top ∧ ∀𝑠
∈ 𝒫 (𝐽
↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪
𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽
↾t 𝑆) =
∪ 𝑡)))) |
11 | 10 | bicomd 226 |
. . . 4
⊢ ((𝐽 ↾t 𝑆) ∈ Top → (((𝐽 ↾t 𝑆) ∈ Top ∧ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪
(𝐽 ↾t
𝑆) = ∪ 𝑠
→ ∃𝑡 ∈
(𝒫 𝑠 ∩
Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)) ↔ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪
(𝐽 ↾t
𝑆) = ∪ 𝑠
→ ∃𝑡 ∈
(𝒫 𝑠 ∩
Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))) |
12 | 9, 11 | syl 17 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (((𝐽 ↾t 𝑆) ∈ Top ∧ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪
(𝐽 ↾t
𝑆) = ∪ 𝑠
→ ∃𝑡 ∈
(𝒫 𝑠 ∩
Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)) ↔ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪
(𝐽 ↾t
𝑆) = ∪ 𝑠
→ ∃𝑡 ∈
(𝒫 𝑠 ∩
Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))) |
13 | 2, 12 | syl5bb 286 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Comp ↔ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪
(𝐽 ↾t
𝑆) = ∪ 𝑠
→ ∃𝑡 ∈
(𝒫 𝑠 ∩
Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))) |
14 | | vex 3424 |
. . . . . . . . . . 11
⊢ 𝑡 ∈ V |
15 | | eqeq1 2742 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑡 → (𝑥 = (𝑦 ∩ 𝑆) ↔ 𝑡 = (𝑦 ∩ 𝑆))) |
16 | 15 | rexbidv 3224 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑡 → (∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆) ↔ ∃𝑦 ∈ 𝑐 𝑡 = (𝑦 ∩ 𝑆))) |
17 | 14, 16 | elab 3599 |
. . . . . . . . . 10
⊢ (𝑡 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ ∃𝑦 ∈ 𝑐 𝑡 = (𝑦 ∩ 𝑆)) |
18 | | velpw 4532 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ 𝒫 𝐽 ↔ 𝑐 ⊆ 𝐽) |
19 | | ssel2 3909 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 ⊆ 𝐽 ∧ 𝑦 ∈ 𝑐) → 𝑦 ∈ 𝐽) |
20 | | ineq1 4134 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑑 = 𝑦 → (𝑑 ∩ 𝑆) = (𝑦 ∩ 𝑆)) |
21 | 20 | rspceeqv 3564 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝐽 ∧ 𝑡 = (𝑦 ∩ 𝑆)) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆)) |
22 | 21 | ex 416 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝐽 → (𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆))) |
23 | 19, 22 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 ⊆ 𝐽 ∧ 𝑦 ∈ 𝑐) → (𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆))) |
24 | 23 | ex 416 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ⊆ 𝐽 → (𝑦 ∈ 𝑐 → (𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆)))) |
25 | 18, 24 | sylbi 220 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ 𝒫 𝐽 → (𝑦 ∈ 𝑐 → (𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆)))) |
26 | 25 | adantl 485 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑦 ∈ 𝑐 → (𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆)))) |
27 | 26 | rexlimdv 3210 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∃𝑦 ∈ 𝑐 𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆))) |
28 | | simpll 767 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → 𝐽 ∈ Top) |
29 | 4 | sseq2i 3944 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ⊆ 𝑋 ↔ 𝑆 ⊆ ∪ 𝐽) |
30 | | uniexg 7546 |
. . . . . . . . . . . . . . . 16
⊢ (𝐽 ∈ Top → ∪ 𝐽
∈ V) |
31 | | ssexg 5230 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ⊆ ∪ 𝐽
∧ ∪ 𝐽 ∈ V) → 𝑆 ∈ V) |
32 | 30, 31 | sylan2 596 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ⊆ ∪ 𝐽
∧ 𝐽 ∈ Top) →
𝑆 ∈
V) |
33 | 32 | ancoms 462 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ 𝑆 ∈
V) |
34 | 29, 33 | sylan2b 597 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ∈ V) |
35 | 34 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → 𝑆 ∈ V) |
36 | | elrest 16956 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝑡 ∈ (𝐽 ↾t 𝑆) ↔ ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆))) |
37 | 28, 35, 36 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑡 ∈ (𝐽 ↾t 𝑆) ↔ ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆))) |
38 | 27, 37 | sylibrd 262 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∃𝑦 ∈ 𝑐 𝑡 = (𝑦 ∩ 𝑆) → 𝑡 ∈ (𝐽 ↾t 𝑆))) |
39 | 17, 38 | syl5bi 245 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑡 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → 𝑡 ∈ (𝐽 ↾t 𝑆))) |
40 | 39 | ssrdv 3921 |
. . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ⊆ (𝐽 ↾t 𝑆)) |
41 | | vex 3424 |
. . . . . . . . . 10
⊢ 𝑐 ∈ V |
42 | 41 | abrexex 7753 |
. . . . . . . . 9
⊢ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∈ V |
43 | 42 | elpw 4531 |
. . . . . . . 8
⊢ ({𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∈ 𝒫 (𝐽 ↾t 𝑆) ↔ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ⊆ (𝐽 ↾t 𝑆)) |
44 | 40, 43 | sylibr 237 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∈ 𝒫 (𝐽 ↾t 𝑆)) |
45 | | unieq 4844 |
. . . . . . . . . 10
⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∪ 𝑠 = ∪
{𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)}) |
46 | 45 | eqeq2d 2749 |
. . . . . . . . 9
⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → (∪
(𝐽 ↾t
𝑆) = ∪ 𝑠
↔ ∪ (𝐽 ↾t 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)})) |
47 | | pweq 4543 |
. . . . . . . . . . 11
⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → 𝒫 𝑠 = 𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)}) |
48 | 47 | ineq1d 4140 |
. . . . . . . . . 10
⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → (𝒫 𝑠 ∩ Fin) = (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)) |
49 | 48 | rexeqdv 3338 |
. . . . . . . . 9
⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → (∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡
↔ ∃𝑡 ∈
(𝒫 {𝑥 ∣
∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡)) |
50 | 46, 49 | imbi12d 348 |
. . . . . . . 8
⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ((∪
(𝐽 ↾t
𝑆) = ∪ 𝑠
→ ∃𝑡 ∈
(𝒫 𝑠 ∩
Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡) ↔ (∪ (𝐽
↾t 𝑆) =
∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡))) |
51 | 50 | rspcva 3547 |
. . . . . . 7
⊢ (({𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∈ 𝒫 (𝐽 ↾t 𝑆) ∧ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪
𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽
↾t 𝑆) =
∪ 𝑡)) → (∪
(𝐽 ↾t
𝑆) = ∪ {𝑥
∣ ∃𝑦 ∈
𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡)) |
52 | 44, 51 | sylan 583 |
. . . . . 6
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪
𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽
↾t 𝑆) =
∪ 𝑡)) → (∪
(𝐽 ↾t
𝑆) = ∪ {𝑥
∣ ∃𝑦 ∈
𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡)) |
53 | 52 | ex 416 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪
𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽
↾t 𝑆) =
∪ 𝑡) → (∪ (𝐽 ↾t 𝑆) = ∪
{𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡))) |
54 | 4 | restuni 22083 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 = ∪ (𝐽 ↾t 𝑆)) |
55 | 54 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → 𝑆 = ∪ (𝐽 ↾t 𝑆)) |
56 | | vex 3424 |
. . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V |
57 | 56 | inex1 5224 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∩ 𝑆) ∈ V |
58 | 57 | dfiun2 4956 |
. . . . . . . . . . . 12
⊢ ∪ 𝑦 ∈ 𝑐 (𝑦 ∩ 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} |
59 | | incom 4129 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∩ 𝑆) = (𝑆 ∩ 𝑦) |
60 | 59 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ 𝑦 ∈ 𝑐) → (𝑦 ∩ 𝑆) = (𝑆 ∩ 𝑦)) |
61 | 60 | iuneq2dv 4942 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ∪ 𝑦 ∈ 𝑐 (𝑦 ∩ 𝑆) = ∪
𝑦 ∈ 𝑐 (𝑆 ∩ 𝑦)) |
62 | 58, 61 | eqtr3id 2793 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ∪ {𝑥
∣ ∃𝑦 ∈
𝑐 𝑥 = (𝑦 ∩ 𝑆)} = ∪
𝑦 ∈ 𝑐 (𝑆 ∩ 𝑦)) |
63 | | iunin2 4993 |
. . . . . . . . . . . 12
⊢ ∪ 𝑦 ∈ 𝑐 (𝑆 ∩ 𝑦) = (𝑆 ∩ ∪
𝑦 ∈ 𝑐 𝑦) |
64 | | uniiun 4981 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑐 =
∪ 𝑦 ∈ 𝑐 𝑦 |
65 | 64 | eqcomi 2747 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑦 ∈ 𝑐 𝑦 = ∪ 𝑐 |
66 | 65 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ∪ 𝑦 ∈ 𝑐 𝑦 = ∪ 𝑐) |
67 | 66 | ineq2d 4141 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 ∩ ∪
𝑦 ∈ 𝑐 𝑦) = (𝑆 ∩ ∪ 𝑐)) |
68 | | incom 4129 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∩ ∪ 𝑐) =
(∪ 𝑐 ∩ 𝑆) |
69 | | sseqin2 4144 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 ⊆ ∪ 𝑐
↔ (∪ 𝑐 ∩ 𝑆) = 𝑆) |
70 | 69 | biimpi 219 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ⊆ ∪ 𝑐
→ (∪ 𝑐 ∩ 𝑆) = 𝑆) |
71 | 68, 70 | syl5eq 2791 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ⊆ ∪ 𝑐
→ (𝑆 ∩ ∪ 𝑐) =
𝑆) |
72 | 71 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 ∩ ∪ 𝑐) = 𝑆) |
73 | 67, 72 | eqtrd 2778 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 ∩ ∪
𝑦 ∈ 𝑐 𝑦) = 𝑆) |
74 | 63, 73 | syl5eq 2791 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ∪ 𝑦 ∈ 𝑐 (𝑆 ∩ 𝑦) = 𝑆) |
75 | 62, 74 | eqtr2d 2779 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → 𝑆 = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)}) |
76 | 55, 75 | eqeq12d 2754 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 = 𝑆 ↔ ∪ (𝐽 ↾t 𝑆) = ∪
{𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)})) |
77 | 55 | eqeq1d 2740 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 = ∪ 𝑡 ↔ ∪ (𝐽
↾t 𝑆) =
∪ 𝑡)) |
78 | 77 | rexbidv 3224 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡 ↔ ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡)) |
79 | 76, 78 | imbi12d 348 |
. . . . . . . 8
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ((𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡) ↔ (∪ (𝐽
↾t 𝑆) =
∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡))) |
80 | | eqid 2738 |
. . . . . . . . . 10
⊢ 𝑆 = 𝑆 |
81 | 80 | a1bi 366 |
. . . . . . . . 9
⊢
(∃𝑡 ∈
(𝒫 {𝑥 ∣
∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡 ↔ (𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡)) |
82 | | elin 3896 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin) ↔ (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∧ 𝑡 ∈ Fin)) |
83 | | velpw 4532 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ 𝑡 ⊆ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)}) |
84 | | dfss3 3902 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ⊆ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ ∀𝑠 ∈ 𝑡 𝑠 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)}) |
85 | | vex 3424 |
. . . . . . . . . . . . . . . 16
⊢ 𝑠 ∈ V |
86 | | eqeq1 2742 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑠 → (𝑥 = (𝑦 ∩ 𝑆) ↔ 𝑠 = (𝑦 ∩ 𝑆))) |
87 | 86 | rexbidv 3224 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑠 → (∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆) ↔ ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆))) |
88 | 85, 87 | elab 3599 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆)) |
89 | 88 | ralbii 3089 |
. . . . . . . . . . . . . 14
⊢
(∀𝑠 ∈
𝑡 𝑠 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ ∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆)) |
90 | 83, 84, 89 | 3bitri 300 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ ∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆)) |
91 | 90 | anbi1i 627 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∧ 𝑡 ∈ Fin) ↔ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) |
92 | 82, 91 | bitri 278 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin) ↔ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) |
93 | | ineq1 4134 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑓‘𝑠) → (𝑦 ∩ 𝑆) = ((𝑓‘𝑠) ∩ 𝑆)) |
94 | 93 | eqeq2d 2749 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑓‘𝑠) → (𝑠 = (𝑦 ∩ 𝑆) ↔ 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) |
95 | 94 | ac6sfi 8939 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ Fin ∧ ∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆)) → ∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) |
96 | 95 | ancoms 462 |
. . . . . . . . . . . . 13
⊢
((∀𝑠 ∈
𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin) → ∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) |
97 | 96 | adantl 485 |
. . . . . . . . . . . 12
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) → ∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) |
98 | | frn 6570 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓:𝑡⟶𝑐 → ran 𝑓 ⊆ 𝑐) |
99 | 98 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ran 𝑓 ⊆ 𝑐) |
100 | | vex 3424 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑓 ∈ V |
101 | 100 | rnex 7708 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ran 𝑓 ∈ V |
102 | 101 | elpw 4531 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ran
𝑓 ∈ 𝒫 𝑐 ↔ ran 𝑓 ⊆ 𝑐) |
103 | 99, 102 | sylibr 237 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ran 𝑓 ∈ 𝒫 𝑐) |
104 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) → 𝑡 ∈ Fin) |
105 | 104 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → 𝑡 ∈ Fin) |
106 | | ffn 6563 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓:𝑡⟶𝑐 → 𝑓 Fn 𝑡) |
107 | | dffn4 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 Fn 𝑡 ↔ 𝑓:𝑡–onto→ran 𝑓) |
108 | 106, 107 | sylib 221 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓:𝑡⟶𝑐 → 𝑓:𝑡–onto→ran 𝑓) |
109 | | fodomfi 8973 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑡 ∈ Fin ∧ 𝑓:𝑡–onto→ran 𝑓) → ran 𝑓 ≼ 𝑡) |
110 | 108, 109 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑡 ∈ Fin ∧ 𝑓:𝑡⟶𝑐) → ran 𝑓 ≼ 𝑡) |
111 | 110 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((∀𝑠 ∈
𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin) ∧ 𝑓:𝑡⟶𝑐) → ran 𝑓 ≼ 𝑡) |
112 | 111 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑓:𝑡⟶𝑐) → ran 𝑓 ≼ 𝑡) |
113 | 112 | ad2ant2r 747 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ran 𝑓 ≼ 𝑡) |
114 | | domfi 8920 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑡 ∈ Fin ∧ ran 𝑓 ≼ 𝑡) → ran 𝑓 ∈ Fin) |
115 | 105, 113,
114 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ran 𝑓 ∈ Fin) |
116 | 103, 115 | elind 4122 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin)) |
117 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑠 = 𝑢 → 𝑠 = 𝑢) |
118 | | fveq2 6735 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑠 = 𝑢 → (𝑓‘𝑠) = (𝑓‘𝑢)) |
119 | 118 | ineq1d 4140 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑠 = 𝑢 → ((𝑓‘𝑠) ∩ 𝑆) = ((𝑓‘𝑢) ∩ 𝑆)) |
120 | 117, 119 | eqeq12d 2754 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑠 = 𝑢 → (𝑠 = ((𝑓‘𝑠) ∩ 𝑆) ↔ 𝑢 = ((𝑓‘𝑢) ∩ 𝑆))) |
121 | 120 | rspccv 3546 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∀𝑠 ∈
𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆) → (𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆))) |
122 | | pm2.27 42 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑢 ∈ 𝑡 → ((𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)) → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆))) |
123 | | inss1 4157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑓‘𝑢) ∩ 𝑆) ⊆ (𝑓‘𝑢) |
124 | | sseq1 3940 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑢 = ((𝑓‘𝑢) ∩ 𝑆) → (𝑢 ⊆ (𝑓‘𝑢) ↔ ((𝑓‘𝑢) ∩ 𝑆) ⊆ (𝑓‘𝑢))) |
125 | 123, 124 | mpbiri 261 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑢 = ((𝑓‘𝑢) ∩ 𝑆) → 𝑢 ⊆ (𝑓‘𝑢)) |
126 | | ssel 3907 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑢 ⊆ (𝑓‘𝑢) → (𝑤 ∈ 𝑢 → 𝑤 ∈ (𝑓‘𝑢))) |
127 | 126 | a1dd 50 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑢 ⊆ (𝑓‘𝑢) → (𝑤 ∈ 𝑢 → (𝑓:𝑡⟶𝑐 → 𝑤 ∈ (𝑓‘𝑢)))) |
128 | 125, 127 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑢 = ((𝑓‘𝑢) ∩ 𝑆) → (𝑤 ∈ 𝑢 → (𝑓:𝑡⟶𝑐 → 𝑤 ∈ (𝑓‘𝑢)))) |
129 | 128 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑢 ∈ 𝑡 → (𝑢 = ((𝑓‘𝑢) ∩ 𝑆) → (𝑤 ∈ 𝑢 → (𝑓:𝑡⟶𝑐 → 𝑤 ∈ (𝑓‘𝑢))))) |
130 | 129 | 3imp 1113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑢 ∈ 𝑡 ∧ 𝑢 = ((𝑓‘𝑢) ∩ 𝑆) ∧ 𝑤 ∈ 𝑢) → (𝑓:𝑡⟶𝑐 → 𝑤 ∈ (𝑓‘𝑢))) |
131 | | fnfvelrn 6919 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑓 Fn 𝑡 ∧ 𝑢 ∈ 𝑡) → (𝑓‘𝑢) ∈ ran 𝑓) |
132 | 131 | expcom 417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑢 ∈ 𝑡 → (𝑓 Fn 𝑡 → (𝑓‘𝑢) ∈ ran 𝑓)) |
133 | 132 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑢 ∈ 𝑡 ∧ 𝑢 = ((𝑓‘𝑢) ∩ 𝑆) ∧ 𝑤 ∈ 𝑢) → (𝑓 Fn 𝑡 → (𝑓‘𝑢) ∈ ran 𝑓)) |
134 | 106, 133 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑢 ∈ 𝑡 ∧ 𝑢 = ((𝑓‘𝑢) ∩ 𝑆) ∧ 𝑤 ∈ 𝑢) → (𝑓:𝑡⟶𝑐 → (𝑓‘𝑢) ∈ ran 𝑓)) |
135 | 130, 134 | jcad 516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑢 ∈ 𝑡 ∧ 𝑢 = ((𝑓‘𝑢) ∩ 𝑆) ∧ 𝑤 ∈ 𝑢) → (𝑓:𝑡⟶𝑐 → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓))) |
136 | 135 | 3exp 1121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑢 ∈ 𝑡 → (𝑢 = ((𝑓‘𝑢) ∩ 𝑆) → (𝑤 ∈ 𝑢 → (𝑓:𝑡⟶𝑐 → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓))))) |
137 | 122, 136 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑢 ∈ 𝑡 → ((𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)) → (𝑤 ∈ 𝑢 → (𝑓:𝑡⟶𝑐 → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓))))) |
138 | 137 | com3r 87 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 ∈ 𝑢 → (𝑢 ∈ 𝑡 → ((𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)) → (𝑓:𝑡⟶𝑐 → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓))))) |
139 | 138 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → ((𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)) → (𝑓:𝑡⟶𝑐 → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓)))) |
140 | 139 | com3l 89 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)) → (𝑓:𝑡⟶𝑐 → ((𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓)))) |
141 | 140 | impcom 411 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑓:𝑡⟶𝑐 ∧ (𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆))) → ((𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓))) |
142 | 121, 141 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → ((𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓))) |
143 | | fvex 6748 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓‘𝑢) ∈ V |
144 | | eleq2 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑣 = (𝑓‘𝑢) → (𝑤 ∈ 𝑣 ↔ 𝑤 ∈ (𝑓‘𝑢))) |
145 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑣 = (𝑓‘𝑢) → (𝑣 ∈ ran 𝑓 ↔ (𝑓‘𝑢) ∈ ran 𝑓)) |
146 | 144, 145 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑣 = (𝑓‘𝑢) → ((𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓) ↔ (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓))) |
147 | 143, 146 | spcev 3533 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓) → ∃𝑣(𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓)) |
148 | 142, 147 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → ((𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → ∃𝑣(𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓))) |
149 | 148 | exlimdv 1941 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → (∃𝑢(𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → ∃𝑣(𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓))) |
150 | | eluni 4836 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ ∪ 𝑡
↔ ∃𝑢(𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡)) |
151 | | eluni 4836 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ ∪ ran 𝑓 ↔ ∃𝑣(𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓)) |
152 | 149, 150,
151 | 3imtr4g 299 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → (𝑤 ∈ ∪ 𝑡 → 𝑤 ∈ ∪ ran
𝑓)) |
153 | 152 | ssrdv 3921 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → ∪ 𝑡 ⊆ ∪ ran 𝑓) |
154 | 153 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ∪
𝑡 ⊆ ∪ ran 𝑓) |
155 | | sseq1 3940 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑆 = ∪
𝑡 → (𝑆 ⊆ ∪ ran
𝑓 ↔ ∪ 𝑡
⊆ ∪ ran 𝑓)) |
156 | 155 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → (𝑆 ⊆ ∪ ran
𝑓 ↔ ∪ 𝑡
⊆ ∪ ran 𝑓)) |
157 | 154, 156 | mpbird 260 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → 𝑆 ⊆ ∪ ran
𝑓) |
158 | 116, 157 | jca 515 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran
𝑓)) |
159 | 158 | ex 416 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) → ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran
𝑓))) |
160 | 159 | eximdv 1925 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) → (∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran
𝑓))) |
161 | 160 | ex 416 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) → (𝑆 = ∪ 𝑡 → (∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran
𝑓)))) |
162 | 161 | com23 86 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) → (∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → (𝑆 = ∪ 𝑡 → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran
𝑓)))) |
163 | | unieq 4844 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = ran 𝑓 → ∪ 𝑑 = ∪
ran 𝑓) |
164 | 163 | sseq2d 3947 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = ran 𝑓 → (𝑆 ⊆ ∪ 𝑑 ↔ 𝑆 ⊆ ∪ ran
𝑓)) |
165 | 164 | rspcev 3549 |
. . . . . . . . . . . . . 14
⊢ ((ran
𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran 𝑓) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) |
166 | 165 | exlimiv 1938 |
. . . . . . . . . . . . 13
⊢
(∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran 𝑓) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) |
167 | 162, 166 | syl8 76 |
. . . . . . . . . . . 12
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) → (∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → (𝑆 = ∪ 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑))) |
168 | 97, 167 | mpd 15 |
. . . . . . . . . . 11
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) → (𝑆 = ∪ 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)) |
169 | 92, 168 | sylan2b 597 |
. . . . . . . . . 10
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ 𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)) → (𝑆 = ∪ 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)) |
170 | 169 | rexlimdva 3211 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)) |
171 | 81, 170 | syl5bir 246 |
. . . . . . . 8
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ((𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)) |
172 | 79, 171 | sylbird 263 |
. . . . . . 7
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ((∪ (𝐽
↾t 𝑆) =
∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡)
→ ∃𝑑 ∈
(𝒫 𝑐 ∩
Fin)𝑆 ⊆ ∪ 𝑑)) |
173 | 172 | ex 416 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑆 ⊆ ∪ 𝑐 → ((∪ (𝐽
↾t 𝑆) =
∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡)
→ ∃𝑑 ∈
(𝒫 𝑐 ∩
Fin)𝑆 ⊆ ∪ 𝑑))) |
174 | 173 | com23 86 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → ((∪
(𝐽 ↾t
𝑆) = ∪ {𝑥
∣ ∃𝑦 ∈
𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡)
→ (𝑆 ⊆ ∪ 𝑐
→ ∃𝑑 ∈
(𝒫 𝑐 ∩
Fin)𝑆 ⊆ ∪ 𝑑))) |
175 | 53, 174 | syld 47 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪
𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽
↾t 𝑆) =
∪ 𝑡) → (𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑))) |
176 | 175 | ralrimdva 3111 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪
𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽
↾t 𝑆) =
∪ 𝑡) → ∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑))) |
177 | 4 | cmpsublem 22320 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪
(𝐽 ↾t
𝑆) = ∪ 𝑠
→ ∃𝑡 ∈
(𝒫 𝑠 ∩
Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))) |
178 | 176, 177 | impbid 215 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪
𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽
↾t 𝑆) =
∪ 𝑡) ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑))) |
179 | 13, 178 | bitrd 282 |
1
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑))) |