Proof of Theorem gchxpidm
| Step | Hyp | Ref
| Expression |
| 1 | | 0ex 5307 |
. . . . . . . 8
⊢ ∅
∈ V |
| 2 | 1 | a1i 11 |
. . . . . . 7
⊢ (¬
𝐴 ∈ Fin → ∅
∈ V) |
| 3 | | xpsneng 9096 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ ∅ ∈
V) → (𝐴 ×
{∅}) ≈ 𝐴) |
| 4 | 2, 3 | sylan2 593 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 × {∅}) ≈
𝐴) |
| 5 | 4 | ensymd 9045 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ≈ (𝐴 × {∅})) |
| 6 | | df1o2 8513 |
. . . . . . 7
⊢
1o = {∅} |
| 7 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝐴 = ∅ → 𝐴 = ∅) |
| 8 | | 0fi 9082 |
. . . . . . . . . . . 12
⊢ ∅
∈ Fin |
| 9 | 7, 8 | eqeltrdi 2849 |
. . . . . . . . . . 11
⊢ (𝐴 = ∅ → 𝐴 ∈ Fin) |
| 10 | 9 | necon3bi 2967 |
. . . . . . . . . 10
⊢ (¬
𝐴 ∈ Fin → 𝐴 ≠ ∅) |
| 11 | 10 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ≠ ∅) |
| 12 | | 0sdomg 9144 |
. . . . . . . . . 10
⊢ (𝐴 ∈ GCH → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
| 13 | 12 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
| 14 | 11, 13 | mpbird 257 |
. . . . . . . 8
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → ∅
≺ 𝐴) |
| 15 | | 0sdom1dom 9274 |
. . . . . . . 8
⊢ (∅
≺ 𝐴 ↔
1o ≼ 𝐴) |
| 16 | 14, 15 | sylib 218 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) →
1o ≼ 𝐴) |
| 17 | 6, 16 | eqbrtrrid 5179 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → {∅}
≼ 𝐴) |
| 18 | | xpdom2g 9108 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ {∅}
≼ 𝐴) → (𝐴 × {∅}) ≼
(𝐴 × 𝐴)) |
| 19 | 17, 18 | syldan 591 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 × {∅}) ≼
(𝐴 × 𝐴)) |
| 20 | | endomtr 9052 |
. . . . 5
⊢ ((𝐴 ≈ (𝐴 × {∅}) ∧ (𝐴 × {∅}) ≼ (𝐴 × 𝐴)) → 𝐴 ≼ (𝐴 × 𝐴)) |
| 21 | 5, 19, 20 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ≼ (𝐴 × 𝐴)) |
| 22 | | canth2g 9171 |
. . . . . . . . . 10
⊢ (𝐴 ∈ GCH → 𝐴 ≺ 𝒫 𝐴) |
| 23 | 22 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ≺ 𝒫 𝐴) |
| 24 | | sdomdom 9020 |
. . . . . . . . 9
⊢ (𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴) |
| 25 | 23, 24 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ≼ 𝒫 𝐴) |
| 26 | | xpdom1g 9109 |
. . . . . . . 8
⊢ ((𝐴 ∈ GCH ∧ 𝐴 ≼ 𝒫 𝐴) → (𝐴 × 𝐴) ≼ (𝒫 𝐴 × 𝐴)) |
| 27 | 25, 26 | syldan 591 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 × 𝐴) ≼ (𝒫 𝐴 × 𝐴)) |
| 28 | | pwexg 5378 |
. . . . . . . . 9
⊢ (𝐴 ∈ GCH → 𝒫
𝐴 ∈
V) |
| 29 | 28 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝒫
𝐴 ∈
V) |
| 30 | | xpdom2g 9108 |
. . . . . . . 8
⊢
((𝒫 𝐴 ∈
V ∧ 𝐴 ≼ 𝒫
𝐴) → (𝒫 𝐴 × 𝐴) ≼ (𝒫 𝐴 × 𝒫 𝐴)) |
| 31 | 29, 25, 30 | syl2anc 584 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝒫
𝐴 × 𝐴) ≼ (𝒫 𝐴 × 𝒫 𝐴)) |
| 32 | | domtr 9047 |
. . . . . . 7
⊢ (((𝐴 × 𝐴) ≼ (𝒫 𝐴 × 𝐴) ∧ (𝒫 𝐴 × 𝐴) ≼ (𝒫 𝐴 × 𝒫 𝐴)) → (𝐴 × 𝐴) ≼ (𝒫 𝐴 × 𝒫 𝐴)) |
| 33 | 27, 31, 32 | syl2anc 584 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 × 𝐴) ≼ (𝒫 𝐴 × 𝒫 𝐴)) |
| 34 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ∈ GCH) |
| 35 | | pwdjuen 10222 |
. . . . . . . . 9
⊢ ((𝐴 ∈ GCH ∧ 𝐴 ∈ GCH) → 𝒫
(𝐴 ⊔ 𝐴) ≈ (𝒫 𝐴 × 𝒫 𝐴)) |
| 36 | 34, 35 | syldan 591 |
. . . . . . . 8
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝒫
(𝐴 ⊔ 𝐴) ≈ (𝒫 𝐴 × 𝒫 𝐴)) |
| 37 | 36 | ensymd 9045 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝒫
𝐴 × 𝒫 𝐴) ≈ 𝒫 (𝐴 ⊔ 𝐴)) |
| 38 | | gchdjuidm 10708 |
. . . . . . . 8
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ⊔ 𝐴) ≈ 𝐴) |
| 39 | | pwen 9190 |
. . . . . . . 8
⊢ ((𝐴 ⊔ 𝐴) ≈ 𝐴 → 𝒫 (𝐴 ⊔ 𝐴) ≈ 𝒫 𝐴) |
| 40 | 38, 39 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝒫
(𝐴 ⊔ 𝐴) ≈ 𝒫 𝐴) |
| 41 | | entr 9046 |
. . . . . . 7
⊢
(((𝒫 𝐴
× 𝒫 𝐴)
≈ 𝒫 (𝐴
⊔ 𝐴) ∧ 𝒫
(𝐴 ⊔ 𝐴) ≈ 𝒫 𝐴) → (𝒫 𝐴 × 𝒫 𝐴) ≈ 𝒫 𝐴) |
| 42 | 37, 40, 41 | syl2anc 584 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝒫
𝐴 × 𝒫 𝐴) ≈ 𝒫 𝐴) |
| 43 | | domentr 9053 |
. . . . . 6
⊢ (((𝐴 × 𝐴) ≼ (𝒫 𝐴 × 𝒫 𝐴) ∧ (𝒫 𝐴 × 𝒫 𝐴) ≈ 𝒫 𝐴) → (𝐴 × 𝐴) ≼ 𝒫 𝐴) |
| 44 | 33, 42, 43 | syl2anc 584 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 × 𝐴) ≼ 𝒫 𝐴) |
| 45 | | gchinf 10697 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → ω
≼ 𝐴) |
| 46 | | pwxpndom 10706 |
. . . . . . 7
⊢ (ω
≼ 𝐴 → ¬
𝒫 𝐴 ≼ (𝐴 × 𝐴)) |
| 47 | 45, 46 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → ¬
𝒫 𝐴 ≼ (𝐴 × 𝐴)) |
| 48 | | ensym 9043 |
. . . . . . 7
⊢ ((𝐴 × 𝐴) ≈ 𝒫 𝐴 → 𝒫 𝐴 ≈ (𝐴 × 𝐴)) |
| 49 | | endom 9019 |
. . . . . . 7
⊢
(𝒫 𝐴 ≈
(𝐴 × 𝐴) → 𝒫 𝐴 ≼ (𝐴 × 𝐴)) |
| 50 | 48, 49 | syl 17 |
. . . . . 6
⊢ ((𝐴 × 𝐴) ≈ 𝒫 𝐴 → 𝒫 𝐴 ≼ (𝐴 × 𝐴)) |
| 51 | 47, 50 | nsyl 140 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → ¬ (𝐴 × 𝐴) ≈ 𝒫 𝐴) |
| 52 | | brsdom 9015 |
. . . . 5
⊢ ((𝐴 × 𝐴) ≺ 𝒫 𝐴 ↔ ((𝐴 × 𝐴) ≼ 𝒫 𝐴 ∧ ¬ (𝐴 × 𝐴) ≈ 𝒫 𝐴)) |
| 53 | 44, 51, 52 | sylanbrc 583 |
. . . 4
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 × 𝐴) ≺ 𝒫 𝐴) |
| 54 | 21, 53 | jca 511 |
. . 3
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ≼ (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ≺ 𝒫 𝐴)) |
| 55 | | gchen1 10665 |
. . 3
⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≼ (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ≺ 𝒫 𝐴)) → 𝐴 ≈ (𝐴 × 𝐴)) |
| 56 | 54, 55 | mpdan 687 |
. 2
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ≈ (𝐴 × 𝐴)) |
| 57 | 56 | ensymd 9045 |
1
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 × 𝐴) ≈ 𝐴) |