Proof of Theorem fnemeet1
| Step | Hyp | Ref
| Expression |
| 1 | | unitg 22974 |
. . . . . . . 8
⊢ (𝑡 ∈ 𝑆 → ∪
(topGen‘𝑡) = ∪ 𝑡) |
| 2 | 1 | adantl 481 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) ∧ 𝑡 ∈ 𝑆) → ∪
(topGen‘𝑡) = ∪ 𝑡) |
| 3 | | unieq 4918 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑡 → ∪ 𝑦 = ∪
𝑡) |
| 4 | 3 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝑦 = 𝑡 → (𝑋 = ∪ 𝑦 ↔ 𝑋 = ∪ 𝑡)) |
| 5 | 4 | rspccva 3621 |
. . . . . . . 8
⊢
((∀𝑦 ∈
𝑆 𝑋 = ∪ 𝑦 ∧ 𝑡 ∈ 𝑆) → 𝑋 = ∪ 𝑡) |
| 6 | 5 | 3ad2antl2 1187 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) ∧ 𝑡 ∈ 𝑆) → 𝑋 = ∪ 𝑡) |
| 7 | 2, 6 | eqtr4d 2780 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) ∧ 𝑡 ∈ 𝑆) → ∪
(topGen‘𝑡) = 𝑋) |
| 8 | | eqimss 4042 |
. . . . . 6
⊢ (∪ (topGen‘𝑡) = 𝑋 → ∪
(topGen‘𝑡) ⊆
𝑋) |
| 9 | 7, 8 | syl 17 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) ∧ 𝑡 ∈ 𝑆) → ∪
(topGen‘𝑡) ⊆
𝑋) |
| 10 | | sspwuni 5100 |
. . . . 5
⊢
((topGen‘𝑡)
⊆ 𝒫 𝑋 ↔
∪ (topGen‘𝑡) ⊆ 𝑋) |
| 11 | 9, 10 | sylibr 234 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) ∧ 𝑡 ∈ 𝑆) → (topGen‘𝑡) ⊆ 𝒫 𝑋) |
| 12 | 11 | ralrimiva 3146 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) → ∀𝑡 ∈ 𝑆 (topGen‘𝑡) ⊆ 𝒫 𝑋) |
| 13 | | ne0i 4341 |
. . . 4
⊢ (𝐴 ∈ 𝑆 → 𝑆 ≠ ∅) |
| 14 | 13 | 3ad2ant3 1136 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) → 𝑆 ≠ ∅) |
| 15 | | riinn0 5083 |
. . 3
⊢
((∀𝑡 ∈
𝑆 (topGen‘𝑡) ⊆ 𝒫 𝑋 ∧ 𝑆 ≠ ∅) → (𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 (topGen‘𝑡)) = ∩
𝑡 ∈ 𝑆 (topGen‘𝑡)) |
| 16 | 12, 14, 15 | syl2anc 584 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) → (𝒫 𝑋 ∩ ∩
𝑡 ∈ 𝑆 (topGen‘𝑡)) = ∩
𝑡 ∈ 𝑆 (topGen‘𝑡)) |
| 17 | | simp3 1139 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) → 𝐴 ∈ 𝑆) |
| 18 | | ssid 4006 |
. . . . . . . 8
⊢
(topGen‘𝐴)
⊆ (topGen‘𝐴) |
| 19 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑡 = 𝐴 → (topGen‘𝑡) = (topGen‘𝐴)) |
| 20 | 19 | sseq1d 4015 |
. . . . . . . . 9
⊢ (𝑡 = 𝐴 → ((topGen‘𝑡) ⊆ (topGen‘𝐴) ↔ (topGen‘𝐴) ⊆ (topGen‘𝐴))) |
| 21 | 20 | rspcev 3622 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑆 ∧ (topGen‘𝐴) ⊆ (topGen‘𝐴)) → ∃𝑡 ∈ 𝑆 (topGen‘𝑡) ⊆ (topGen‘𝐴)) |
| 22 | 17, 18, 21 | sylancl 586 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) → ∃𝑡 ∈ 𝑆 (topGen‘𝑡) ⊆ (topGen‘𝐴)) |
| 23 | | iinss 5056 |
. . . . . . 7
⊢
(∃𝑡 ∈
𝑆 (topGen‘𝑡) ⊆ (topGen‘𝐴) → ∩ 𝑡 ∈ 𝑆 (topGen‘𝑡) ⊆ (topGen‘𝐴)) |
| 24 | 22, 23 | syl 17 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) → ∩
𝑡 ∈ 𝑆 (topGen‘𝑡) ⊆ (topGen‘𝐴)) |
| 25 | 24 | unissd 4917 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) → ∪
∩ 𝑡 ∈ 𝑆 (topGen‘𝑡) ⊆ ∪
(topGen‘𝐴)) |
| 26 | | unitg 22974 |
. . . . . 6
⊢ (𝐴 ∈ 𝑆 → ∪
(topGen‘𝐴) = ∪ 𝐴) |
| 27 | 26 | 3ad2ant3 1136 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) → ∪
(topGen‘𝐴) = ∪ 𝐴) |
| 28 | 25, 27 | sseqtrd 4020 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) → ∪
∩ 𝑡 ∈ 𝑆 (topGen‘𝑡) ⊆ ∪ 𝐴) |
| 29 | | unieq 4918 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝐴 → ∪ 𝑦 = ∪
𝐴) |
| 30 | 29 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝐴 → (𝑋 = ∪ 𝑦 ↔ 𝑋 = ∪ 𝐴)) |
| 31 | 30 | rspccva 3621 |
. . . . . . . . . . 11
⊢
((∀𝑦 ∈
𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) → 𝑋 = ∪ 𝐴) |
| 32 | 31 | 3adant1 1131 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) → 𝑋 = ∪ 𝐴) |
| 33 | 32 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) ∧ 𝑡 ∈ 𝑆) → 𝑋 = ∪ 𝐴) |
| 34 | 33, 6 | eqtr3d 2779 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) ∧ 𝑡 ∈ 𝑆) → ∪ 𝐴 = ∪
𝑡) |
| 35 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) ∧ 𝑡 ∈ 𝑆) → 𝑡 ∈ 𝑆) |
| 36 | | ssid 4006 |
. . . . . . . . 9
⊢ 𝑡 ⊆ 𝑡 |
| 37 | | eltg3i 22968 |
. . . . . . . . 9
⊢ ((𝑡 ∈ 𝑆 ∧ 𝑡 ⊆ 𝑡) → ∪ 𝑡 ∈ (topGen‘𝑡)) |
| 38 | 35, 36, 37 | sylancl 586 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) ∧ 𝑡 ∈ 𝑆) → ∪ 𝑡 ∈ (topGen‘𝑡)) |
| 39 | 34, 38 | eqeltrd 2841 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) ∧ 𝑡 ∈ 𝑆) → ∪ 𝐴 ∈ (topGen‘𝑡)) |
| 40 | 39 | ralrimiva 3146 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) → ∀𝑡 ∈ 𝑆 ∪ 𝐴 ∈ (topGen‘𝑡)) |
| 41 | | uniexg 7760 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑆 → ∪ 𝐴 ∈ V) |
| 42 | 41 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) → ∪ 𝐴 ∈ V) |
| 43 | | eliin 4996 |
. . . . . . 7
⊢ (∪ 𝐴
∈ V → (∪ 𝐴 ∈ ∩
𝑡 ∈ 𝑆 (topGen‘𝑡) ↔ ∀𝑡 ∈ 𝑆 ∪ 𝐴 ∈ (topGen‘𝑡))) |
| 44 | 42, 43 | syl 17 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) → (∪ 𝐴 ∈ ∩ 𝑡 ∈ 𝑆 (topGen‘𝑡) ↔ ∀𝑡 ∈ 𝑆 ∪ 𝐴 ∈ (topGen‘𝑡))) |
| 45 | 40, 44 | mpbird 257 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) → ∪ 𝐴 ∈ ∩ 𝑡 ∈ 𝑆 (topGen‘𝑡)) |
| 46 | | elssuni 4937 |
. . . . 5
⊢ (∪ 𝐴
∈ ∩ 𝑡 ∈ 𝑆 (topGen‘𝑡) → ∪ 𝐴 ⊆ ∪ ∩ 𝑡 ∈ 𝑆 (topGen‘𝑡)) |
| 47 | 45, 46 | syl 17 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) → ∪ 𝐴 ⊆ ∪ ∩ 𝑡 ∈ 𝑆 (topGen‘𝑡)) |
| 48 | 28, 47 | eqssd 4001 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) → ∪
∩ 𝑡 ∈ 𝑆 (topGen‘𝑡) = ∪ 𝐴) |
| 49 | | eqid 2737 |
. . . 4
⊢ ∪ ∩ 𝑡 ∈ 𝑆 (topGen‘𝑡) = ∪ ∩ 𝑡 ∈ 𝑆 (topGen‘𝑡) |
| 50 | | eqid 2737 |
. . . 4
⊢ ∪ 𝐴 =
∪ 𝐴 |
| 51 | 49, 50 | isfne4 36341 |
. . 3
⊢ (∩ 𝑡 ∈ 𝑆 (topGen‘𝑡)Fne𝐴 ↔ (∪
∩ 𝑡 ∈ 𝑆 (topGen‘𝑡) = ∪ 𝐴 ∧ ∩ 𝑡 ∈ 𝑆 (topGen‘𝑡) ⊆ (topGen‘𝐴))) |
| 52 | 48, 24, 51 | sylanbrc 583 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) → ∩
𝑡 ∈ 𝑆 (topGen‘𝑡)Fne𝐴) |
| 53 | 16, 52 | eqbrtrd 5165 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) → (𝒫 𝑋 ∩ ∩
𝑡 ∈ 𝑆 (topGen‘𝑡))Fne𝐴) |