Step |
Hyp |
Ref |
Expression |
1 |
|
hmphdis.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
|
dfsn2 |
⊢ { ∅ } = { ∅ , ∅ } |
3 |
|
indislem |
⊢ { ∅ , ( I ‘ 𝐴 ) } = { ∅ , 𝐴 } |
4 |
|
preq2 |
⊢ ( ( I ‘ 𝐴 ) = ∅ → { ∅ , ( I ‘ 𝐴 ) } = { ∅ , ∅ } ) |
5 |
4 2
|
eqtr4di |
⊢ ( ( I ‘ 𝐴 ) = ∅ → { ∅ , ( I ‘ 𝐴 ) } = { ∅ } ) |
6 |
3 5
|
syl5eqr |
⊢ ( ( I ‘ 𝐴 ) = ∅ → { ∅ , 𝐴 } = { ∅ } ) |
7 |
6
|
breq2d |
⊢ ( ( I ‘ 𝐴 ) = ∅ → ( 𝐽 ≃ { ∅ , 𝐴 } ↔ 𝐽 ≃ { ∅ } ) ) |
8 |
7
|
biimpac |
⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) = ∅ ) → 𝐽 ≃ { ∅ } ) |
9 |
|
hmph0 |
⊢ ( 𝐽 ≃ { ∅ } ↔ 𝐽 = { ∅ } ) |
10 |
8 9
|
sylib |
⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) = ∅ ) → 𝐽 = { ∅ } ) |
11 |
10
|
unieqd |
⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) = ∅ ) → ∪ 𝐽 = ∪ { ∅ } ) |
12 |
|
0ex |
⊢ ∅ ∈ V |
13 |
12
|
unisn |
⊢ ∪ { ∅ } = ∅ |
14 |
13
|
eqcomi |
⊢ ∅ = ∪ { ∅ } |
15 |
11 1 14
|
3eqtr4g |
⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) = ∅ ) → 𝑋 = ∅ ) |
16 |
15
|
preq2d |
⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) = ∅ ) → { ∅ , 𝑋 } = { ∅ , ∅ } ) |
17 |
2 10 16
|
3eqtr4a |
⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) = ∅ ) → 𝐽 = { ∅ , 𝑋 } ) |
18 |
|
hmphen |
⊢ ( 𝐽 ≃ { ∅ , 𝐴 } → 𝐽 ≈ { ∅ , 𝐴 } ) |
19 |
|
necom |
⊢ ( ( I ‘ 𝐴 ) ≠ ∅ ↔ ∅ ≠ ( I ‘ 𝐴 ) ) |
20 |
|
fvex |
⊢ ( I ‘ 𝐴 ) ∈ V |
21 |
|
pr2nelem |
⊢ ( ( ∅ ∈ V ∧ ( I ‘ 𝐴 ) ∈ V ∧ ∅ ≠ ( I ‘ 𝐴 ) ) → { ∅ , ( I ‘ 𝐴 ) } ≈ 2o ) |
22 |
12 20 21
|
mp3an12 |
⊢ ( ∅ ≠ ( I ‘ 𝐴 ) → { ∅ , ( I ‘ 𝐴 ) } ≈ 2o ) |
23 |
19 22
|
sylbi |
⊢ ( ( I ‘ 𝐴 ) ≠ ∅ → { ∅ , ( I ‘ 𝐴 ) } ≈ 2o ) |
24 |
23
|
adantl |
⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) ≠ ∅ ) → { ∅ , ( I ‘ 𝐴 ) } ≈ 2o ) |
25 |
3 24
|
eqbrtrrid |
⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) ≠ ∅ ) → { ∅ , 𝐴 } ≈ 2o ) |
26 |
|
entr |
⊢ ( ( 𝐽 ≈ { ∅ , 𝐴 } ∧ { ∅ , 𝐴 } ≈ 2o ) → 𝐽 ≈ 2o ) |
27 |
18 25 26
|
syl2an2r |
⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) ≠ ∅ ) → 𝐽 ≈ 2o ) |
28 |
|
hmphtop1 |
⊢ ( 𝐽 ≃ { ∅ , 𝐴 } → 𝐽 ∈ Top ) |
29 |
28
|
adantr |
⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) ≠ ∅ ) → 𝐽 ∈ Top ) |
30 |
1
|
toptopon |
⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
31 |
29 30
|
sylib |
⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) ≠ ∅ ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
32 |
|
en2top |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ≈ 2o ↔ ( 𝐽 = { ∅ , 𝑋 } ∧ 𝑋 ≠ ∅ ) ) ) |
33 |
31 32
|
syl |
⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) ≠ ∅ ) → ( 𝐽 ≈ 2o ↔ ( 𝐽 = { ∅ , 𝑋 } ∧ 𝑋 ≠ ∅ ) ) ) |
34 |
27 33
|
mpbid |
⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) ≠ ∅ ) → ( 𝐽 = { ∅ , 𝑋 } ∧ 𝑋 ≠ ∅ ) ) |
35 |
34
|
simpld |
⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) ≠ ∅ ) → 𝐽 = { ∅ , 𝑋 } ) |
36 |
17 35
|
pm2.61dane |
⊢ ( 𝐽 ≃ { ∅ , 𝐴 } → 𝐽 = { ∅ , 𝑋 } ) |