Step | Hyp | Ref
| Expression |
1 | | rabexg 5224 |
. . . . . . 7
⊢ (𝐽 ∈ Top → {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ V) |
2 | 1 | ad2antrr 726 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) → {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ V) |
3 | | ssrab2 3993 |
. . . . . . 7
⊢ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ⊆ 𝐽 |
4 | | elpwg 4516 |
. . . . . . 7
⊢ ({𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ V → ({𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ 𝒫 𝐽 ↔ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ⊆ 𝐽)) |
5 | 3, 4 | mpbiri 261 |
. . . . . 6
⊢ ({𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ V → {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ 𝒫 𝐽) |
6 | 2, 5 | syl 17 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) → {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ 𝒫 𝐽) |
7 | | unieq 4830 |
. . . . . . . 8
⊢ (𝑐 = {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∪ 𝑐 = ∪
{𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}) |
8 | 7 | sseq2d 3933 |
. . . . . . 7
⊢ (𝑐 = {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (𝑆 ⊆ ∪ 𝑐 ↔ 𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})) |
9 | | pweq 4529 |
. . . . . . . . 9
⊢ (𝑐 = {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → 𝒫 𝑐 = 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}) |
10 | 9 | ineq1d 4126 |
. . . . . . . 8
⊢ (𝑐 = {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (𝒫 𝑐 ∩ Fin) = (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)) |
11 | 10 | rexeqdv 3326 |
. . . . . . 7
⊢ (𝑐 = {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑 ↔ ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑)) |
12 | 8, 11 | imbi12d 348 |
. . . . . 6
⊢ (𝑐 = {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ((𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) ↔ (𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑))) |
13 | 12 | rspcva 3535 |
. . . . 5
⊢ (({𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ 𝒫 𝐽 ∧ ∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)) → (𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑)) |
14 | 6, 13 | sylan 583 |
. . . 4
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ ∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)) → (𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑)) |
15 | 14 | ex 416 |
. . 3
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) → (∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) → (𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑))) |
16 | | cmpsub.1 |
. . . . . . . 8
⊢ 𝑋 = ∪
𝐽 |
17 | 16 | restuni 22059 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 = ∪ (𝐽 ↾t 𝑆)) |
18 | 17 | adantr 484 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) → 𝑆 = ∪ (𝐽 ↾t 𝑆)) |
19 | 18 | eqeq1d 2739 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) → (𝑆 = ∪ 𝑠 ↔ ∪ (𝐽
↾t 𝑆) =
∪ 𝑠)) |
20 | | velpw 4518 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆) ↔ 𝑠 ⊆ (𝐽 ↾t 𝑆)) |
21 | | eleq2 2826 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 = ∪
𝑠 → (𝑡 ∈ 𝑆 ↔ 𝑡 ∈ ∪ 𝑠)) |
22 | | eluni 4822 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ ∪ 𝑠
↔ ∃𝑢(𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠)) |
23 | 21, 22 | bitrdi 290 |
. . . . . . . . . . . . . 14
⊢ (𝑆 = ∪
𝑠 → (𝑡 ∈ 𝑆 ↔ ∃𝑢(𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠))) |
24 | 23 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ⊆ (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑡 ∈ 𝑆 ↔ ∃𝑢(𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠))) |
25 | | ssel 3893 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ⊆ (𝐽 ↾t 𝑆) → (𝑢 ∈ 𝑠 → 𝑢 ∈ (𝐽 ↾t 𝑆))) |
26 | 16 | sseq2i 3930 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑆 ⊆ 𝑋 ↔ 𝑆 ⊆ ∪ 𝐽) |
27 | | uniexg 7528 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐽 ∈ Top → ∪ 𝐽
∈ V) |
28 | | ssexg 5216 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆 ⊆ ∪ 𝐽
∧ ∪ 𝐽 ∈ V) → 𝑆 ∈ V) |
29 | 28 | ancoms 462 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((∪ 𝐽
∈ V ∧ 𝑆 ⊆
∪ 𝐽) → 𝑆 ∈ V) |
30 | 27, 29 | sylan 583 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ 𝑆 ∈
V) |
31 | 26, 30 | sylan2b 597 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ∈ V) |
32 | | elrest 16932 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝑢 ∈ (𝐽 ↾t 𝑆) ↔ ∃𝑤 ∈ 𝐽 𝑢 = (𝑤 ∩ 𝑆))) |
33 | 31, 32 | syldan 594 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑢 ∈ (𝐽 ↾t 𝑆) ↔ ∃𝑤 ∈ 𝐽 𝑢 = (𝑤 ∩ 𝑆))) |
34 | | inss1 4143 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑤 ∩ 𝑆) ⊆ 𝑤 |
35 | | sseq1 3926 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑢 = (𝑤 ∩ 𝑆) → (𝑢 ⊆ 𝑤 ↔ (𝑤 ∩ 𝑆) ⊆ 𝑤)) |
36 | 34, 35 | mpbiri 261 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑢 = (𝑤 ∩ 𝑆) → 𝑢 ⊆ 𝑤) |
37 | 36 | sselda 3901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑢 = (𝑤 ∩ 𝑆) ∧ 𝑡 ∈ 𝑢) → 𝑡 ∈ 𝑤) |
38 | 37 | 3ad2antl3 1189 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑡 ∈ 𝑢) → 𝑡 ∈ 𝑤) |
39 | 38 | 3adant2 1133 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢) → 𝑡 ∈ 𝑤) |
40 | | ineq1 4120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 = 𝑤 → (𝑦 ∩ 𝑆) = (𝑤 ∩ 𝑆)) |
41 | 40 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = 𝑤 → ((𝑦 ∩ 𝑆) ∈ 𝑠 ↔ (𝑤 ∩ 𝑆) ∈ 𝑠)) |
42 | | simp12 1206 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢) → 𝑤 ∈ 𝐽) |
43 | | eleq1 2825 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑢 = (𝑤 ∩ 𝑆) → (𝑢 ∈ 𝑠 ↔ (𝑤 ∩ 𝑆) ∈ 𝑠)) |
44 | 43 | biimpa 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑢 = (𝑤 ∩ 𝑆) ∧ 𝑢 ∈ 𝑠) → (𝑤 ∩ 𝑆) ∈ 𝑠) |
45 | 44 | 3ad2antl3 1189 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑢 ∈ 𝑠) → (𝑤 ∩ 𝑆) ∈ 𝑠) |
46 | 45 | 3adant3 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢) → (𝑤 ∩ 𝑆) ∈ 𝑠) |
47 | 41, 42, 46 | elrabd 3604 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢) → 𝑤 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}) |
48 | | vex 3412 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑤 ∈ V |
49 | | eleq2 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑣 = 𝑤 → (𝑡 ∈ 𝑣 ↔ 𝑡 ∈ 𝑤)) |
50 | | eleq1 2825 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑣 = 𝑤 → (𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ↔ 𝑤 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})) |
51 | 49, 50 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑣 = 𝑤 → ((𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}) ↔ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))) |
52 | 48, 51 | spcev 3521 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑡 ∈ 𝑤 ∧ 𝑤 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}) → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})) |
53 | 39, 47, 52 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢) → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})) |
54 | 53 | 3exp 1121 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) → (𝑢 ∈ 𝑠 → (𝑡 ∈ 𝑢 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))) |
55 | 54 | rexlimdv3a 3205 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∃𝑤 ∈ 𝐽 𝑢 = (𝑤 ∩ 𝑆) → (𝑢 ∈ 𝑠 → (𝑡 ∈ 𝑢 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))))) |
56 | 33, 55 | sylbid 243 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑢 ∈ (𝐽 ↾t 𝑆) → (𝑢 ∈ 𝑠 → (𝑡 ∈ 𝑢 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))))) |
57 | 56 | com23 86 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑢 ∈ 𝑠 → (𝑢 ∈ (𝐽 ↾t 𝑆) → (𝑡 ∈ 𝑢 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))))) |
58 | 57 | com4l 92 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ 𝑠 → (𝑢 ∈ (𝐽 ↾t 𝑆) → (𝑡 ∈ 𝑢 → ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))))) |
59 | 25, 58 | sylcom 30 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ⊆ (𝐽 ↾t 𝑆) → (𝑢 ∈ 𝑠 → (𝑡 ∈ 𝑢 → ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))))) |
60 | 59 | com24 95 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 ⊆ (𝐽 ↾t 𝑆) → ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑡 ∈ 𝑢 → (𝑢 ∈ 𝑠 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))))) |
61 | 60 | impcom 411 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ⊆ (𝐽 ↾t 𝑆)) → (𝑡 ∈ 𝑢 → (𝑢 ∈ 𝑠 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))) |
62 | 61 | impd 414 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ⊆ (𝐽 ↾t 𝑆)) → ((𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠) → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))) |
63 | 62 | exlimdv 1941 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ⊆ (𝐽 ↾t 𝑆)) → (∃𝑢(𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠) → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))) |
64 | 63 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ⊆ (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (∃𝑢(𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠) → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))) |
65 | 24, 64 | sylbid 243 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ⊆ (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑡 ∈ 𝑆 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))) |
66 | 65 | ex 416 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ⊆ (𝐽 ↾t 𝑆)) → (𝑆 = ∪ 𝑠 → (𝑡 ∈ 𝑆 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))) |
67 | 20, 66 | sylan2b 597 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) → (𝑆 = ∪ 𝑠 → (𝑡 ∈ 𝑆 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))) |
68 | 67 | imp 410 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑡 ∈ 𝑆 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))) |
69 | | eluni 4822 |
. . . . . . . . 9
⊢ (𝑡 ∈ ∪ {𝑦
∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ↔ ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})) |
70 | 68, 69 | syl6ibr 255 |
. . . . . . . 8
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑡 ∈ 𝑆 → 𝑡 ∈ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})) |
71 | 70 | ssrdv 3907 |
. . . . . . 7
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → 𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}) |
72 | | pm2.27 42 |
. . . . . . . . 9
⊢ (𝑆 ⊆ ∪ {𝑦
∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ((𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑)) |
73 | | elin 3882 |
. . . . . . . . . . 11
⊢ (𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin) ↔ (𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin)) |
74 | | vex 3412 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑡 ∈ V |
75 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑡 → (𝑥 = (𝑧 ∩ 𝑆) ↔ 𝑡 = (𝑧 ∩ 𝑆))) |
76 | 75 | rexbidv 3216 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑡 → (∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆) ↔ ∃𝑧 ∈ 𝑑 𝑡 = (𝑧 ∩ 𝑆))) |
77 | 74, 76 | elab 3587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 ∈ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ↔ ∃𝑧 ∈ 𝑑 𝑡 = (𝑧 ∩ 𝑆)) |
78 | | velpw 4518 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ↔ 𝑑 ⊆ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}) |
79 | | ssel 3893 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑑 ⊆ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (𝑧 ∈ 𝑑 → 𝑧 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})) |
80 | | ineq1 4120 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = 𝑧 → (𝑦 ∩ 𝑆) = (𝑧 ∩ 𝑆)) |
81 | 80 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = 𝑧 → ((𝑦 ∩ 𝑆) ∈ 𝑠 ↔ (𝑧 ∩ 𝑆) ∈ 𝑠)) |
82 | 81 | elrab 3602 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ↔ (𝑧 ∈ 𝐽 ∧ (𝑧 ∩ 𝑆) ∈ 𝑠)) |
83 | | eleq1a 2833 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∩ 𝑆) ∈ 𝑠 → (𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠)) |
84 | 82, 83 | simplbiim 508 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠)) |
85 | 79, 84 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑑 ⊆ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (𝑧 ∈ 𝑑 → (𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠))) |
86 | 85 | 2a1d 26 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑑 ⊆ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (𝑆 ⊆ ∪ 𝑑 → ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑧 ∈ 𝑑 → (𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠))))) |
87 | 86 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑑 ⊆ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) → (𝑆 ⊆ ∪ 𝑑 → ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑧 ∈ 𝑑 → (𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠))))) |
88 | 78, 87 | sylanb 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) → (𝑆 ⊆ ∪ 𝑑 → ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑧 ∈ 𝑑 → (𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠))))) |
89 | 88 | 3imp 1113 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → (𝑧 ∈ 𝑑 → (𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠))) |
90 | 89 | rexlimdv 3202 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → (∃𝑧 ∈ 𝑑 𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠)) |
91 | 77, 90 | syl5bi 245 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → (𝑡 ∈ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} → 𝑡 ∈ 𝑠)) |
92 | 91 | ssrdv 3907 |
. . . . . . . . . . . . . . 15
⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ⊆ 𝑠) |
93 | | vex 3412 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑑 ∈ V |
94 | 93 | abrexex 7735 |
. . . . . . . . . . . . . . . 16
⊢ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ V |
95 | 94 | elpw 4517 |
. . . . . . . . . . . . . . 15
⊢ ({𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ 𝒫 𝑠 ↔ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ⊆ 𝑠) |
96 | 92, 95 | sylibr 237 |
. . . . . . . . . . . . . 14
⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ 𝒫 𝑠) |
97 | | abrexfi 8976 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 ∈ Fin → {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ Fin) |
98 | 97 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑) → {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ Fin) |
99 | 98 | 3adant3 1134 |
. . . . . . . . . . . . . 14
⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ Fin) |
100 | 96, 99 | elind 4108 |
. . . . . . . . . . . . 13
⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ (𝒫 𝑠 ∩ Fin)) |
101 | | dfss 3884 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑆 ⊆ ∪ 𝑑
↔ 𝑆 = (𝑆 ∩ ∪ 𝑑)) |
102 | 101 | biimpi 219 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 ⊆ ∪ 𝑑
→ 𝑆 = (𝑆 ∩ ∪ 𝑑)) |
103 | | uniiun 4967 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ 𝑑 =
∪ 𝑧 ∈ 𝑑 𝑧 |
104 | 103 | ineq2i 4124 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑆 ∩ ∪ 𝑑) =
(𝑆 ∩ ∪ 𝑧 ∈ 𝑑 𝑧) |
105 | | iunin2 4979 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑧 ∈ 𝑑 (𝑆 ∩ 𝑧) = (𝑆 ∩ ∪
𝑧 ∈ 𝑑 𝑧) |
106 | | incom 4115 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑆 ∩ 𝑧) = (𝑧 ∩ 𝑆) |
107 | 106 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝑑 → (𝑆 ∩ 𝑧) = (𝑧 ∩ 𝑆)) |
108 | 107 | iuneq2i 4925 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑧 ∈ 𝑑 (𝑆 ∩ 𝑧) = ∪ 𝑧 ∈ 𝑑 (𝑧 ∩ 𝑆) |
109 | 104, 105,
108 | 3eqtr2i 2771 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 ∩ ∪ 𝑑) =
∪ 𝑧 ∈ 𝑑 (𝑧 ∩ 𝑆) |
110 | 102, 109 | eqtrdi 2794 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ⊆ ∪ 𝑑
→ 𝑆 = ∪ 𝑧 ∈ 𝑑 (𝑧 ∩ 𝑆)) |
111 | 110 | 3ad2ant2 1136 |
. . . . . . . . . . . . . 14
⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → 𝑆 = ∪ 𝑧 ∈ 𝑑 (𝑧 ∩ 𝑆)) |
112 | 18 | ad2antrl 728 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ⊆ ∪ 𝑑
∧ (((𝐽 ∈ Top ∧
𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → 𝑆 = ∪ (𝐽 ↾t 𝑆)) |
113 | 112 | 3adant1 1132 |
. . . . . . . . . . . . . 14
⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → 𝑆 = ∪ (𝐽 ↾t 𝑆)) |
114 | | vex 3412 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ V |
115 | 114 | inex1 5210 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∩ 𝑆) ∈ V |
116 | 115 | dfiun2 4942 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑧 ∈ 𝑑 (𝑧 ∩ 𝑆) = ∪ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} |
117 | 116 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → ∪ 𝑧 ∈ 𝑑 (𝑧 ∩ 𝑆) = ∪ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)}) |
118 | 111, 113,
117 | 3eqtr3d 2785 |
. . . . . . . . . . . . 13
⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → ∪ (𝐽
↾t 𝑆) =
∪ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)}) |
119 | | unieq 4830 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} → ∪ 𝑡 = ∪
{𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)}) |
120 | 119 | rspceeqv 3552 |
. . . . . . . . . . . . 13
⊢ (({𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ (𝒫 𝑠 ∩ Fin) ∧ ∪ (𝐽
↾t 𝑆) =
∪ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)}) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡) |
121 | 100, 118,
120 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽
↾t 𝑆) =
∪ 𝑡) |
122 | 121 | 3exp 1121 |
. . . . . . . . . . 11
⊢ ((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) → (𝑆 ⊆ ∪ 𝑑 → ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽
↾t 𝑆) =
∪ 𝑡))) |
123 | 73, 122 | sylbi 220 |
. . . . . . . . . 10
⊢ (𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin) → (𝑆 ⊆ ∪ 𝑑 → ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽
↾t 𝑆) =
∪ 𝑡))) |
124 | 123 | rexlimiv 3199 |
. . . . . . . . 9
⊢
(∃𝑑 ∈
(𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑 → ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽
↾t 𝑆) =
∪ 𝑡)) |
125 | 72, 124 | syl6 35 |
. . . . . . . 8
⊢ (𝑆 ⊆ ∪ {𝑦
∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ((𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽
↾t 𝑆) =
∪ 𝑡))) |
126 | 125 | com3r 87 |
. . . . . . 7
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ((𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽
↾t 𝑆) =
∪ 𝑡))) |
127 | 71, 126 | mpd 15 |
. . . . . 6
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → ((𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽
↾t 𝑆) =
∪ 𝑡)) |
128 | 127 | ex 416 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) → (𝑆 = ∪ 𝑠 → ((𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽
↾t 𝑆) =
∪ 𝑡))) |
129 | 19, 128 | sylbird 263 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) → (∪
(𝐽 ↾t
𝑆) = ∪ 𝑠
→ ((𝑆 ⊆ ∪ {𝑦
∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽
↾t 𝑆) =
∪ 𝑡))) |
130 | 129 | com23 86 |
. . 3
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) → ((𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑) → (∪ (𝐽
↾t 𝑆) =
∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡))) |
131 | 15, 130 | syld 47 |
. 2
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)) → (∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) → (∪ (𝐽
↾t 𝑆) =
∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪
(𝐽 ↾t
𝑆) = ∪ 𝑡))) |
132 | 131 | ralrimdva 3110 |
1
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪
(𝐽 ↾t
𝑆) = ∪ 𝑠
→ ∃𝑡 ∈
(𝒫 𝑠 ∩
Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))) |