Step |
Hyp |
Ref |
Expression |
1 |
|
elssuni |
⊢ ( 𝐴 ∈ 𝑆 → 𝐴 ⊆ ∪ 𝑆 ) |
2 |
1
|
3ad2ant3 |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → 𝐴 ⊆ ∪ 𝑆 ) |
3 |
2
|
unissd |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ∪ 𝐴 ⊆ ∪ ∪ 𝑆 ) |
4 |
|
eqimss2 |
⊢ ( 𝑋 = ∪ 𝑦 → ∪ 𝑦 ⊆ 𝑋 ) |
5 |
|
sspwuni |
⊢ ( 𝑦 ⊆ 𝒫 𝑋 ↔ ∪ 𝑦 ⊆ 𝑋 ) |
6 |
4 5
|
sylibr |
⊢ ( 𝑋 = ∪ 𝑦 → 𝑦 ⊆ 𝒫 𝑋 ) |
7 |
6
|
ralimi |
⊢ ( ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 → ∀ 𝑦 ∈ 𝑆 𝑦 ⊆ 𝒫 𝑋 ) |
8 |
7
|
3ad2ant2 |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ∀ 𝑦 ∈ 𝑆 𝑦 ⊆ 𝒫 𝑋 ) |
9 |
|
unissb |
⊢ ( ∪ 𝑆 ⊆ 𝒫 𝑋 ↔ ∀ 𝑦 ∈ 𝑆 𝑦 ⊆ 𝒫 𝑋 ) |
10 |
8 9
|
sylibr |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ∪ 𝑆 ⊆ 𝒫 𝑋 ) |
11 |
|
sspwuni |
⊢ ( ∪ 𝑆 ⊆ 𝒫 𝑋 ↔ ∪ ∪ 𝑆 ⊆ 𝑋 ) |
12 |
10 11
|
sylib |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ∪ ∪ 𝑆 ⊆ 𝑋 ) |
13 |
|
unieq |
⊢ ( 𝑦 = 𝐴 → ∪ 𝑦 = ∪ 𝐴 ) |
14 |
13
|
eqeq2d |
⊢ ( 𝑦 = 𝐴 → ( 𝑋 = ∪ 𝑦 ↔ 𝑋 = ∪ 𝐴 ) ) |
15 |
14
|
rspccva |
⊢ ( ( ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → 𝑋 = ∪ 𝐴 ) |
16 |
15
|
3adant1 |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → 𝑋 = ∪ 𝐴 ) |
17 |
12 16
|
sseqtrd |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ∪ ∪ 𝑆 ⊆ ∪ 𝐴 ) |
18 |
3 17
|
eqssd |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ∪ 𝐴 = ∪ ∪ 𝑆 ) |
19 |
|
pwexg |
⊢ ( 𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ V ) |
20 |
19
|
3ad2ant1 |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → 𝒫 𝑋 ∈ V ) |
21 |
20 10
|
ssexd |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ∪ 𝑆 ∈ V ) |
22 |
|
bastg |
⊢ ( ∪ 𝑆 ∈ V → ∪ 𝑆 ⊆ ( topGen ‘ ∪ 𝑆 ) ) |
23 |
21 22
|
syl |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ∪ 𝑆 ⊆ ( topGen ‘ ∪ 𝑆 ) ) |
24 |
2 23
|
sstrd |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → 𝐴 ⊆ ( topGen ‘ ∪ 𝑆 ) ) |
25 |
|
eqid |
⊢ ∪ 𝐴 = ∪ 𝐴 |
26 |
|
eqid |
⊢ ∪ ∪ 𝑆 = ∪ ∪ 𝑆 |
27 |
25 26
|
isfne4 |
⊢ ( 𝐴 Fne ∪ 𝑆 ↔ ( ∪ 𝐴 = ∪ ∪ 𝑆 ∧ 𝐴 ⊆ ( topGen ‘ ∪ 𝑆 ) ) ) |
28 |
18 24 27
|
sylanbrc |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → 𝐴 Fne ∪ 𝑆 ) |
29 |
|
ne0i |
⊢ ( 𝐴 ∈ 𝑆 → 𝑆 ≠ ∅ ) |
30 |
29
|
3ad2ant3 |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → 𝑆 ≠ ∅ ) |
31 |
|
ifnefalse |
⊢ ( 𝑆 ≠ ∅ → if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) = ∪ 𝑆 ) |
32 |
30 31
|
syl |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) = ∪ 𝑆 ) |
33 |
28 32
|
breqtrrd |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → 𝐴 Fne if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) ) |