Proof of Theorem hmphindis
Step | Hyp | Ref
| Expression |
1 | | dfsn2 4580 |
. . 3
⊢ {∅}
= {∅, ∅} |
2 | | indislem 21608 |
. . . . . . 7
⊢ {∅,
( I ‘𝐴)} = {∅,
𝐴} |
3 | | preq2 4670 |
. . . . . . . 8
⊢ (( I
‘𝐴) = ∅ →
{∅, ( I ‘𝐴)} =
{∅, ∅}) |
4 | 3, 1 | syl6eqr 2874 |
. . . . . . 7
⊢ (( I
‘𝐴) = ∅ →
{∅, ( I ‘𝐴)} =
{∅}) |
5 | 2, 4 | syl5eqr 2870 |
. . . . . 6
⊢ (( I
‘𝐴) = ∅ →
{∅, 𝐴} =
{∅}) |
6 | 5 | breq2d 5078 |
. . . . 5
⊢ (( I
‘𝐴) = ∅ →
(𝐽 ≃ {∅, 𝐴} ↔ 𝐽 ≃ {∅})) |
7 | 6 | biimpac 481 |
. . . 4
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) = ∅) → 𝐽 ≃
{∅}) |
8 | | hmph0 22403 |
. . . 4
⊢ (𝐽 ≃ {∅} ↔ 𝐽 = {∅}) |
9 | 7, 8 | sylib 220 |
. . 3
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) = ∅) → 𝐽 = {∅}) |
10 | 9 | unieqd 4852 |
. . . . 5
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) = ∅) → ∪ 𝐽 =
∪ {∅}) |
11 | | hmphdis.1 |
. . . . 5
⊢ 𝑋 = ∪
𝐽 |
12 | | 0ex 5211 |
. . . . . . 7
⊢ ∅
∈ V |
13 | 12 | unisn 4858 |
. . . . . 6
⊢ ∪ {∅} = ∅ |
14 | 13 | eqcomi 2830 |
. . . . 5
⊢ ∅ =
∪ {∅} |
15 | 10, 11, 14 | 3eqtr4g 2881 |
. . . 4
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) = ∅) → 𝑋 = ∅) |
16 | 15 | preq2d 4676 |
. . 3
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) = ∅) → {∅,
𝑋} = {∅,
∅}) |
17 | 1, 9, 16 | 3eqtr4a 2882 |
. 2
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) = ∅) → 𝐽 = {∅, 𝑋}) |
18 | | hmphen 22393 |
. . . . 5
⊢ (𝐽 ≃ {∅, 𝐴} → 𝐽 ≈ {∅, 𝐴}) |
19 | | necom 3069 |
. . . . . . . 8
⊢ (( I
‘𝐴) ≠ ∅
↔ ∅ ≠ ( I ‘𝐴)) |
20 | | fvex 6683 |
. . . . . . . . 9
⊢ ( I
‘𝐴) ∈
V |
21 | | pr2nelem 9430 |
. . . . . . . . 9
⊢ ((∅
∈ V ∧ ( I ‘𝐴) ∈ V ∧ ∅ ≠ ( I
‘𝐴)) → {∅,
( I ‘𝐴)} ≈
2o) |
22 | 12, 20, 21 | mp3an12 1447 |
. . . . . . . 8
⊢ (∅
≠ ( I ‘𝐴) →
{∅, ( I ‘𝐴)}
≈ 2o) |
23 | 19, 22 | sylbi 219 |
. . . . . . 7
⊢ (( I
‘𝐴) ≠ ∅
→ {∅, ( I ‘𝐴)} ≈ 2o) |
24 | 23 | adantl 484 |
. . . . . 6
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → {∅,
( I ‘𝐴)} ≈
2o) |
25 | 2, 24 | eqbrtrrid 5102 |
. . . . 5
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → {∅,
𝐴} ≈
2o) |
26 | | entr 8561 |
. . . . 5
⊢ ((𝐽 ≈ {∅, 𝐴} ∧ {∅, 𝐴} ≈ 2o) →
𝐽 ≈
2o) |
27 | 18, 25, 26 | syl2an2r 683 |
. . . 4
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → 𝐽 ≈
2o) |
28 | | hmphtop1 22387 |
. . . . . . 7
⊢ (𝐽 ≃ {∅, 𝐴} → 𝐽 ∈ Top) |
29 | 28 | adantr 483 |
. . . . . 6
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → 𝐽 ∈ Top) |
30 | 11 | toptopon 21525 |
. . . . . 6
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
31 | 29, 30 | sylib 220 |
. . . . 5
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → 𝐽 ∈ (TopOn‘𝑋)) |
32 | | en2top 21593 |
. . . . 5
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ≈ 2o ↔ (𝐽 = {∅, 𝑋} ∧ 𝑋 ≠ ∅))) |
33 | 31, 32 | syl 17 |
. . . 4
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → (𝐽 ≈ 2o ↔
(𝐽 = {∅, 𝑋} ∧ 𝑋 ≠ ∅))) |
34 | 27, 33 | mpbid 234 |
. . 3
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → (𝐽 = {∅, 𝑋} ∧ 𝑋 ≠ ∅)) |
35 | 34 | simpld 497 |
. 2
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → 𝐽 = {∅, 𝑋}) |
36 | 17, 35 | pm2.61dane 3104 |
1
⊢ (𝐽 ≃ {∅, 𝐴} → 𝐽 = {∅, 𝑋}) |