Proof of Theorem hmphindis
| Step | Hyp | Ref
| Expression |
| 1 | | dfsn2 4639 |
. . 3
⊢ {∅}
= {∅, ∅} |
| 2 | | indislem 23007 |
. . . . . . 7
⊢ {∅,
( I ‘𝐴)} = {∅,
𝐴} |
| 3 | | preq2 4734 |
. . . . . . . 8
⊢ (( I
‘𝐴) = ∅ →
{∅, ( I ‘𝐴)} =
{∅, ∅}) |
| 4 | 3, 1 | eqtr4di 2795 |
. . . . . . 7
⊢ (( I
‘𝐴) = ∅ →
{∅, ( I ‘𝐴)} =
{∅}) |
| 5 | 2, 4 | eqtr3id 2791 |
. . . . . 6
⊢ (( I
‘𝐴) = ∅ →
{∅, 𝐴} =
{∅}) |
| 6 | 5 | breq2d 5155 |
. . . . 5
⊢ (( I
‘𝐴) = ∅ →
(𝐽 ≃ {∅, 𝐴} ↔ 𝐽 ≃ {∅})) |
| 7 | 6 | biimpac 478 |
. . . 4
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) = ∅) → 𝐽 ≃
{∅}) |
| 8 | | hmph0 23803 |
. . . 4
⊢ (𝐽 ≃ {∅} ↔ 𝐽 = {∅}) |
| 9 | 7, 8 | sylib 218 |
. . 3
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) = ∅) → 𝐽 = {∅}) |
| 10 | 9 | unieqd 4920 |
. . . . 5
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) = ∅) → ∪ 𝐽 =
∪ {∅}) |
| 11 | | hmphdis.1 |
. . . . 5
⊢ 𝑋 = ∪
𝐽 |
| 12 | | 0ex 5307 |
. . . . . . 7
⊢ ∅
∈ V |
| 13 | 12 | unisn 4926 |
. . . . . 6
⊢ ∪ {∅} = ∅ |
| 14 | 13 | eqcomi 2746 |
. . . . 5
⊢ ∅ =
∪ {∅} |
| 15 | 10, 11, 14 | 3eqtr4g 2802 |
. . . 4
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) = ∅) → 𝑋 = ∅) |
| 16 | 15 | preq2d 4740 |
. . 3
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) = ∅) → {∅,
𝑋} = {∅,
∅}) |
| 17 | 1, 9, 16 | 3eqtr4a 2803 |
. 2
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) = ∅) → 𝐽 = {∅, 𝑋}) |
| 18 | | hmphen 23793 |
. . . . 5
⊢ (𝐽 ≃ {∅, 𝐴} → 𝐽 ≈ {∅, 𝐴}) |
| 19 | | necom 2994 |
. . . . . . . 8
⊢ (( I
‘𝐴) ≠ ∅
↔ ∅ ≠ ( I ‘𝐴)) |
| 20 | | fvex 6919 |
. . . . . . . . 9
⊢ ( I
‘𝐴) ∈
V |
| 21 | | enpr2 10042 |
. . . . . . . . 9
⊢ ((∅
∈ V ∧ ( I ‘𝐴) ∈ V ∧ ∅ ≠ ( I
‘𝐴)) → {∅,
( I ‘𝐴)} ≈
2o) |
| 22 | 12, 20, 21 | mp3an12 1453 |
. . . . . . . 8
⊢ (∅
≠ ( I ‘𝐴) →
{∅, ( I ‘𝐴)}
≈ 2o) |
| 23 | 19, 22 | sylbi 217 |
. . . . . . 7
⊢ (( I
‘𝐴) ≠ ∅
→ {∅, ( I ‘𝐴)} ≈ 2o) |
| 24 | 23 | adantl 481 |
. . . . . 6
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → {∅,
( I ‘𝐴)} ≈
2o) |
| 25 | 2, 24 | eqbrtrrid 5179 |
. . . . 5
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → {∅,
𝐴} ≈
2o) |
| 26 | | entr 9046 |
. . . . 5
⊢ ((𝐽 ≈ {∅, 𝐴} ∧ {∅, 𝐴} ≈ 2o) →
𝐽 ≈
2o) |
| 27 | 18, 25, 26 | syl2an2r 685 |
. . . 4
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → 𝐽 ≈
2o) |
| 28 | | hmphtop1 23787 |
. . . . . . 7
⊢ (𝐽 ≃ {∅, 𝐴} → 𝐽 ∈ Top) |
| 29 | 28 | adantr 480 |
. . . . . 6
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → 𝐽 ∈ Top) |
| 30 | 11 | toptopon 22923 |
. . . . . 6
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
| 31 | 29, 30 | sylib 218 |
. . . . 5
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → 𝐽 ∈ (TopOn‘𝑋)) |
| 32 | | en2top 22992 |
. . . . 5
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ≈ 2o ↔ (𝐽 = {∅, 𝑋} ∧ 𝑋 ≠ ∅))) |
| 33 | 31, 32 | syl 17 |
. . . 4
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → (𝐽 ≈ 2o ↔
(𝐽 = {∅, 𝑋} ∧ 𝑋 ≠ ∅))) |
| 34 | 27, 33 | mpbid 232 |
. . 3
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → (𝐽 = {∅, 𝑋} ∧ 𝑋 ≠ ∅)) |
| 35 | 34 | simpld 494 |
. 2
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → 𝐽 = {∅, 𝑋}) |
| 36 | 17, 35 | pm2.61dane 3029 |
1
⊢ (𝐽 ≃ {∅, 𝐴} → 𝐽 = {∅, 𝑋}) |