Proof of Theorem gchxpidm
Step | Hyp | Ref
| Expression |
1 | | 0ex 5200 |
. . . . . . . 8
⊢ ∅
∈ V |
2 | 1 | a1i 11 |
. . . . . . 7
⊢ (¬
𝐴 ∈ Fin → ∅
∈ V) |
3 | | xpsneng 8730 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ ∅ ∈
V) → (𝐴 ×
{∅}) ≈ 𝐴) |
4 | 2, 3 | sylan2 596 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 × {∅}) ≈
𝐴) |
5 | 4 | ensymd 8679 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ≈ (𝐴 × {∅})) |
6 | | df1o2 8214 |
. . . . . . 7
⊢
1o = {∅} |
7 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝐴 = ∅ → 𝐴 = ∅) |
8 | | 0fin 8849 |
. . . . . . . . . . . 12
⊢ ∅
∈ Fin |
9 | 7, 8 | eqeltrdi 2846 |
. . . . . . . . . . 11
⊢ (𝐴 = ∅ → 𝐴 ∈ Fin) |
10 | 9 | necon3bi 2967 |
. . . . . . . . . 10
⊢ (¬
𝐴 ∈ Fin → 𝐴 ≠ ∅) |
11 | 10 | adantl 485 |
. . . . . . . . 9
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ≠ ∅) |
12 | | 0sdomg 8775 |
. . . . . . . . . 10
⊢ (𝐴 ∈ GCH → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
13 | 12 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
14 | 11, 13 | mpbird 260 |
. . . . . . . 8
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → ∅
≺ 𝐴) |
15 | | 0sdom1dom 8876 |
. . . . . . . 8
⊢ (∅
≺ 𝐴 ↔
1o ≼ 𝐴) |
16 | 14, 15 | sylib 221 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) →
1o ≼ 𝐴) |
17 | 6, 16 | eqbrtrrid 5089 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → {∅}
≼ 𝐴) |
18 | | xpdom2g 8741 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ {∅}
≼ 𝐴) → (𝐴 × {∅}) ≼
(𝐴 × 𝐴)) |
19 | 17, 18 | syldan 594 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 × {∅}) ≼
(𝐴 × 𝐴)) |
20 | | endomtr 8686 |
. . . . 5
⊢ ((𝐴 ≈ (𝐴 × {∅}) ∧ (𝐴 × {∅}) ≼ (𝐴 × 𝐴)) → 𝐴 ≼ (𝐴 × 𝐴)) |
21 | 5, 19, 20 | syl2anc 587 |
. . . 4
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ≼ (𝐴 × 𝐴)) |
22 | | canth2g 8800 |
. . . . . . . . . 10
⊢ (𝐴 ∈ GCH → 𝐴 ≺ 𝒫 𝐴) |
23 | 22 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ≺ 𝒫 𝐴) |
24 | | sdomdom 8656 |
. . . . . . . . 9
⊢ (𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴) |
25 | 23, 24 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ≼ 𝒫 𝐴) |
26 | | xpdom1g 8742 |
. . . . . . . 8
⊢ ((𝐴 ∈ GCH ∧ 𝐴 ≼ 𝒫 𝐴) → (𝐴 × 𝐴) ≼ (𝒫 𝐴 × 𝐴)) |
27 | 25, 26 | syldan 594 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 × 𝐴) ≼ (𝒫 𝐴 × 𝐴)) |
28 | | pwexg 5271 |
. . . . . . . . 9
⊢ (𝐴 ∈ GCH → 𝒫
𝐴 ∈
V) |
29 | 28 | adantr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝒫
𝐴 ∈
V) |
30 | | xpdom2g 8741 |
. . . . . . . 8
⊢
((𝒫 𝐴 ∈
V ∧ 𝐴 ≼ 𝒫
𝐴) → (𝒫 𝐴 × 𝐴) ≼ (𝒫 𝐴 × 𝒫 𝐴)) |
31 | 29, 25, 30 | syl2anc 587 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝒫
𝐴 × 𝐴) ≼ (𝒫 𝐴 × 𝒫 𝐴)) |
32 | | domtr 8681 |
. . . . . . 7
⊢ (((𝐴 × 𝐴) ≼ (𝒫 𝐴 × 𝐴) ∧ (𝒫 𝐴 × 𝐴) ≼ (𝒫 𝐴 × 𝒫 𝐴)) → (𝐴 × 𝐴) ≼ (𝒫 𝐴 × 𝒫 𝐴)) |
33 | 27, 31, 32 | syl2anc 587 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 × 𝐴) ≼ (𝒫 𝐴 × 𝒫 𝐴)) |
34 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ∈ GCH) |
35 | | pwdjuen 9795 |
. . . . . . . . 9
⊢ ((𝐴 ∈ GCH ∧ 𝐴 ∈ GCH) → 𝒫
(𝐴 ⊔ 𝐴) ≈ (𝒫 𝐴 × 𝒫 𝐴)) |
36 | 34, 35 | syldan 594 |
. . . . . . . 8
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝒫
(𝐴 ⊔ 𝐴) ≈ (𝒫 𝐴 × 𝒫 𝐴)) |
37 | 36 | ensymd 8679 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝒫
𝐴 × 𝒫 𝐴) ≈ 𝒫 (𝐴 ⊔ 𝐴)) |
38 | | gchdjuidm 10282 |
. . . . . . . 8
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ⊔ 𝐴) ≈ 𝐴) |
39 | | pwen 8819 |
. . . . . . . 8
⊢ ((𝐴 ⊔ 𝐴) ≈ 𝐴 → 𝒫 (𝐴 ⊔ 𝐴) ≈ 𝒫 𝐴) |
40 | 38, 39 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝒫
(𝐴 ⊔ 𝐴) ≈ 𝒫 𝐴) |
41 | | entr 8680 |
. . . . . . 7
⊢
(((𝒫 𝐴
× 𝒫 𝐴)
≈ 𝒫 (𝐴
⊔ 𝐴) ∧ 𝒫
(𝐴 ⊔ 𝐴) ≈ 𝒫 𝐴) → (𝒫 𝐴 × 𝒫 𝐴) ≈ 𝒫 𝐴) |
42 | 37, 40, 41 | syl2anc 587 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝒫
𝐴 × 𝒫 𝐴) ≈ 𝒫 𝐴) |
43 | | domentr 8687 |
. . . . . 6
⊢ (((𝐴 × 𝐴) ≼ (𝒫 𝐴 × 𝒫 𝐴) ∧ (𝒫 𝐴 × 𝒫 𝐴) ≈ 𝒫 𝐴) → (𝐴 × 𝐴) ≼ 𝒫 𝐴) |
44 | 33, 42, 43 | syl2anc 587 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 × 𝐴) ≼ 𝒫 𝐴) |
45 | | gchinf 10271 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → ω
≼ 𝐴) |
46 | | pwxpndom 10280 |
. . . . . . 7
⊢ (ω
≼ 𝐴 → ¬
𝒫 𝐴 ≼ (𝐴 × 𝐴)) |
47 | 45, 46 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → ¬
𝒫 𝐴 ≼ (𝐴 × 𝐴)) |
48 | | ensym 8677 |
. . . . . . 7
⊢ ((𝐴 × 𝐴) ≈ 𝒫 𝐴 → 𝒫 𝐴 ≈ (𝐴 × 𝐴)) |
49 | | endom 8655 |
. . . . . . 7
⊢
(𝒫 𝐴 ≈
(𝐴 × 𝐴) → 𝒫 𝐴 ≼ (𝐴 × 𝐴)) |
50 | 48, 49 | syl 17 |
. . . . . 6
⊢ ((𝐴 × 𝐴) ≈ 𝒫 𝐴 → 𝒫 𝐴 ≼ (𝐴 × 𝐴)) |
51 | 47, 50 | nsyl 142 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → ¬ (𝐴 × 𝐴) ≈ 𝒫 𝐴) |
52 | | brsdom 8651 |
. . . . 5
⊢ ((𝐴 × 𝐴) ≺ 𝒫 𝐴 ↔ ((𝐴 × 𝐴) ≼ 𝒫 𝐴 ∧ ¬ (𝐴 × 𝐴) ≈ 𝒫 𝐴)) |
53 | 44, 51, 52 | sylanbrc 586 |
. . . 4
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 × 𝐴) ≺ 𝒫 𝐴) |
54 | 21, 53 | jca 515 |
. . 3
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ≼ (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ≺ 𝒫 𝐴)) |
55 | | gchen1 10239 |
. . 3
⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≼ (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ≺ 𝒫 𝐴)) → 𝐴 ≈ (𝐴 × 𝐴)) |
56 | 54, 55 | mpdan 687 |
. 2
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ≈ (𝐴 × 𝐴)) |
57 | 56 | ensymd 8679 |
1
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 × 𝐴) ≈ 𝐴) |