Proof of Theorem hmphindis
Step | Hyp | Ref
| Expression |
1 | | dfsn2 4138 |
. . 3
⊢ {∅}
= {∅, ∅} |
2 | | indislem 20614 |
. . . . . . 7
⊢ {∅,
( I ‘𝐴)} = {∅,
𝐴} |
3 | | preq2 4213 |
. . . . . . . 8
⊢ (( I
‘𝐴) = ∅ →
{∅, ( I ‘𝐴)} =
{∅, ∅}) |
4 | 3, 1 | syl6eqr 2662 |
. . . . . . 7
⊢ (( I
‘𝐴) = ∅ →
{∅, ( I ‘𝐴)} =
{∅}) |
5 | 2, 4 | syl5eqr 2658 |
. . . . . 6
⊢ (( I
‘𝐴) = ∅ →
{∅, 𝐴} =
{∅}) |
6 | 5 | breq2d 4595 |
. . . . 5
⊢ (( I
‘𝐴) = ∅ →
(𝐽 ≃ {∅, 𝐴} ↔ 𝐽 ≃ {∅})) |
7 | 6 | biimpac 502 |
. . . 4
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) = ∅) → 𝐽 ≃
{∅}) |
8 | | hmph0 21408 |
. . . 4
⊢ (𝐽 ≃ {∅} ↔ 𝐽 = {∅}) |
9 | 7, 8 | sylib 207 |
. . 3
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) = ∅) → 𝐽 = {∅}) |
10 | 9 | unieqd 4382 |
. . . . 5
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) = ∅) → ∪ 𝐽 =
∪ {∅}) |
11 | | hmphdis.1 |
. . . . 5
⊢ 𝑋 = ∪
𝐽 |
12 | | 0ex 4718 |
. . . . . . 7
⊢ ∅
∈ V |
13 | 12 | unisn 4387 |
. . . . . 6
⊢ ∪ {∅} = ∅ |
14 | 13 | eqcomi 2619 |
. . . . 5
⊢ ∅ =
∪ {∅} |
15 | 10, 11, 14 | 3eqtr4g 2669 |
. . . 4
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) = ∅) → 𝑋 = ∅) |
16 | 15 | preq2d 4219 |
. . 3
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) = ∅) → {∅,
𝑋} = {∅,
∅}) |
17 | 1, 9, 16 | 3eqtr4a 2670 |
. 2
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) = ∅) → 𝐽 = {∅, 𝑋}) |
18 | | hmphen 21398 |
. . . . . 6
⊢ (𝐽 ≃ {∅, 𝐴} → 𝐽 ≈ {∅, 𝐴}) |
19 | 18 | adantr 480 |
. . . . 5
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → 𝐽 ≈ {∅, 𝐴}) |
20 | | necom 2835 |
. . . . . . . 8
⊢ (( I
‘𝐴) ≠ ∅
↔ ∅ ≠ ( I ‘𝐴)) |
21 | | fvex 6113 |
. . . . . . . . 9
⊢ ( I
‘𝐴) ∈
V |
22 | | pr2nelem 8710 |
. . . . . . . . 9
⊢ ((∅
∈ V ∧ ( I ‘𝐴) ∈ V ∧ ∅ ≠ ( I
‘𝐴)) → {∅,
( I ‘𝐴)} ≈
2𝑜) |
23 | 12, 21, 22 | mp3an12 1406 |
. . . . . . . 8
⊢ (∅
≠ ( I ‘𝐴) →
{∅, ( I ‘𝐴)}
≈ 2𝑜) |
24 | 20, 23 | sylbi 206 |
. . . . . . 7
⊢ (( I
‘𝐴) ≠ ∅
→ {∅, ( I ‘𝐴)} ≈
2𝑜) |
25 | 24 | adantl 481 |
. . . . . 6
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → {∅,
( I ‘𝐴)} ≈
2𝑜) |
26 | 2, 25 | syl5eqbrr 4619 |
. . . . 5
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → {∅,
𝐴} ≈
2𝑜) |
27 | | entr 7894 |
. . . . 5
⊢ ((𝐽 ≈ {∅, 𝐴} ∧ {∅, 𝐴} ≈ 2𝑜)
→ 𝐽 ≈
2𝑜) |
28 | 19, 26, 27 | syl2anc 691 |
. . . 4
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → 𝐽 ≈
2𝑜) |
29 | | hmphtop1 21392 |
. . . . . . 7
⊢ (𝐽 ≃ {∅, 𝐴} → 𝐽 ∈ Top) |
30 | 29 | adantr 480 |
. . . . . 6
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → 𝐽 ∈ Top) |
31 | 11 | toptopon 20548 |
. . . . . 6
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
32 | 30, 31 | sylib 207 |
. . . . 5
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → 𝐽 ∈ (TopOn‘𝑋)) |
33 | | en2top 20600 |
. . . . 5
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ≈ 2𝑜 ↔ (𝐽 = {∅, 𝑋} ∧ 𝑋 ≠ ∅))) |
34 | 32, 33 | syl 17 |
. . . 4
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → (𝐽 ≈ 2𝑜
↔ (𝐽 = {∅, 𝑋} ∧ 𝑋 ≠ ∅))) |
35 | 28, 34 | mpbid 221 |
. . 3
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → (𝐽 = {∅, 𝑋} ∧ 𝑋 ≠ ∅)) |
36 | 35 | simpld 474 |
. 2
⊢ ((𝐽 ≃ {∅, 𝐴} ∧ ( I ‘𝐴) ≠ ∅) → 𝐽 = {∅, 𝑋}) |
37 | 17, 36 | pm2.61dane 2869 |
1
⊢ (𝐽 ≃ {∅, 𝐴} → 𝐽 = {∅, 𝑋}) |