Step | Hyp | Ref
| Expression |
1 | | 1sdom2 8044 |
. . 3
⊢
1𝑜 ≺ 2𝑜 |
2 | | cdaxpdom 8894 |
. . 3
⊢
((1𝑜 ≺ 𝐴 ∧ 1𝑜 ≺
2𝑜) → (𝐴 +𝑐
2𝑜) ≼ (𝐴 ×
2𝑜)) |
3 | 1, 2 | mpan2 703 |
. 2
⊢
(1𝑜 ≺ 𝐴 → (𝐴 +𝑐
2𝑜) ≼ (𝐴 ×
2𝑜)) |
4 | | sdom0 7977 |
. . . . . 6
⊢ ¬
1𝑜 ≺ ∅ |
5 | | breq2 4587 |
. . . . . 6
⊢ (𝐴 = ∅ →
(1𝑜 ≺ 𝐴 ↔ 1𝑜 ≺
∅)) |
6 | 4, 5 | mtbiri 316 |
. . . . 5
⊢ (𝐴 = ∅ → ¬
1𝑜 ≺ 𝐴) |
7 | 6 | con2i 133 |
. . . 4
⊢
(1𝑜 ≺ 𝐴 → ¬ 𝐴 = ∅) |
8 | | neq0 3889 |
. . . 4
⊢ (¬
𝐴 = ∅ ↔
∃𝑥 𝑥 ∈ 𝐴) |
9 | 7, 8 | sylib 207 |
. . 3
⊢
(1𝑜 ≺ 𝐴 → ∃𝑥 𝑥 ∈ 𝐴) |
10 | | relsdom 7848 |
. . . . . . . . . 10
⊢ Rel
≺ |
11 | 10 | brrelex2i 5083 |
. . . . . . . . 9
⊢
(1𝑜 ≺ 𝐴 → 𝐴 ∈ V) |
12 | 11 | adantr 480 |
. . . . . . . 8
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝐴 ∈ V) |
13 | | enrefg 7873 |
. . . . . . . 8
⊢ (𝐴 ∈ V → 𝐴 ≈ 𝐴) |
14 | 12, 13 | syl 17 |
. . . . . . 7
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝐴 ≈ 𝐴) |
15 | | df2o2 7461 |
. . . . . . . . 9
⊢
2𝑜 = {∅, {∅}} |
16 | | pwpw0 4284 |
. . . . . . . . 9
⊢ 𝒫
{∅} = {∅, {∅}} |
17 | 15, 16 | eqtr4i 2635 |
. . . . . . . 8
⊢
2𝑜 = 𝒫 {∅} |
18 | | 0ex 4718 |
. . . . . . . . . 10
⊢ ∅
∈ V |
19 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
20 | | en2sn 7922 |
. . . . . . . . . 10
⊢ ((∅
∈ V ∧ 𝑥 ∈ V)
→ {∅} ≈ {𝑥}) |
21 | 18, 19, 20 | mp2an 704 |
. . . . . . . . 9
⊢ {∅}
≈ {𝑥} |
22 | | pwen 8018 |
. . . . . . . . 9
⊢
({∅} ≈ {𝑥} → 𝒫 {∅} ≈
𝒫 {𝑥}) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . 8
⊢ 𝒫
{∅} ≈ 𝒫 {𝑥} |
24 | 17, 23 | eqbrtri 4604 |
. . . . . . 7
⊢
2𝑜 ≈ 𝒫 {𝑥} |
25 | | xpen 8008 |
. . . . . . 7
⊢ ((𝐴 ≈ 𝐴 ∧ 2𝑜 ≈
𝒫 {𝑥}) →
(𝐴 ×
2𝑜) ≈ (𝐴 × 𝒫 {𝑥})) |
26 | 14, 24, 25 | sylancl 693 |
. . . . . 6
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 × 2𝑜) ≈
(𝐴 × 𝒫 {𝑥})) |
27 | | snex 4835 |
. . . . . . . 8
⊢ {𝑥} ∈ V |
28 | 27 | pwex 4774 |
. . . . . . 7
⊢ 𝒫
{𝑥} ∈
V |
29 | | uncom 3719 |
. . . . . . . . 9
⊢ ((𝐴 ∖ {𝑥}) ∪ {𝑥}) = ({𝑥} ∪ (𝐴 ∖ {𝑥})) |
30 | | simpr 476 |
. . . . . . . . . . 11
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
31 | 30 | snssd 4281 |
. . . . . . . . . 10
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → {𝑥} ⊆ 𝐴) |
32 | | undif 4001 |
. . . . . . . . . 10
⊢ ({𝑥} ⊆ 𝐴 ↔ ({𝑥} ∪ (𝐴 ∖ {𝑥})) = 𝐴) |
33 | 31, 32 | sylib 207 |
. . . . . . . . 9
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → ({𝑥} ∪ (𝐴 ∖ {𝑥})) = 𝐴) |
34 | 29, 33 | syl5eq 2656 |
. . . . . . . 8
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ∖ {𝑥}) ∪ {𝑥}) = 𝐴) |
35 | | difexg 4735 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (𝐴 ∖ {𝑥}) ∈ V) |
36 | 12, 35 | syl 17 |
. . . . . . . . 9
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) ∈ V) |
37 | | canth2g 7999 |
. . . . . . . . 9
⊢ ((𝐴 ∖ {𝑥}) ∈ V → (𝐴 ∖ {𝑥}) ≺ 𝒫 (𝐴 ∖ {𝑥})) |
38 | | domunsn 7995 |
. . . . . . . . 9
⊢ ((𝐴 ∖ {𝑥}) ≺ 𝒫 (𝐴 ∖ {𝑥}) → ((𝐴 ∖ {𝑥}) ∪ {𝑥}) ≼ 𝒫 (𝐴 ∖ {𝑥})) |
39 | 36, 37, 38 | 3syl 18 |
. . . . . . . 8
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ∖ {𝑥}) ∪ {𝑥}) ≼ 𝒫 (𝐴 ∖ {𝑥})) |
40 | 34, 39 | eqbrtrrd 4607 |
. . . . . . 7
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝐴 ≼ 𝒫 (𝐴 ∖ {𝑥})) |
41 | | xpdom1g 7942 |
. . . . . . 7
⊢
((𝒫 {𝑥}
∈ V ∧ 𝐴 ≼
𝒫 (𝐴 ∖ {𝑥})) → (𝐴 × 𝒫 {𝑥}) ≼ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) |
42 | 28, 40, 41 | sylancr 694 |
. . . . . 6
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 × 𝒫 {𝑥}) ≼ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) |
43 | | endomtr 7900 |
. . . . . 6
⊢ (((𝐴 × 2𝑜)
≈ (𝐴 ×
𝒫 {𝑥}) ∧ (𝐴 × 𝒫 {𝑥}) ≼ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) → (𝐴 × 2𝑜) ≼
(𝒫 (𝐴 ∖
{𝑥}) × 𝒫
{𝑥})) |
44 | 26, 42, 43 | syl2anc 691 |
. . . . 5
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 × 2𝑜) ≼
(𝒫 (𝐴 ∖
{𝑥}) × 𝒫
{𝑥})) |
45 | | pwcdaen 8890 |
. . . . . . 7
⊢ (((𝐴 ∖ {𝑥}) ∈ V ∧ {𝑥} ∈ V) → 𝒫 ((𝐴 ∖ {𝑥}) +𝑐 {𝑥}) ≈ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) |
46 | 36, 27, 45 | sylancl 693 |
. . . . . 6
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝒫 ((𝐴 ∖ {𝑥}) +𝑐 {𝑥}) ≈ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) |
47 | 46 | ensymd 7893 |
. . . . 5
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥}) ≈ 𝒫 ((𝐴 ∖ {𝑥}) +𝑐 {𝑥})) |
48 | | domentr 7901 |
. . . . 5
⊢ (((𝐴 × 2𝑜)
≼ (𝒫 (𝐴
∖ {𝑥}) ×
𝒫 {𝑥}) ∧
(𝒫 (𝐴 ∖
{𝑥}) × 𝒫
{𝑥}) ≈ 𝒫
((𝐴 ∖ {𝑥}) +𝑐 {𝑥})) → (𝐴 × 2𝑜) ≼
𝒫 ((𝐴 ∖
{𝑥}) +𝑐
{𝑥})) |
49 | 44, 47, 48 | syl2anc 691 |
. . . 4
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 × 2𝑜) ≼
𝒫 ((𝐴 ∖
{𝑥}) +𝑐
{𝑥})) |
50 | 27 | a1i 11 |
. . . . . . 7
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → {𝑥} ∈ V) |
51 | | incom 3767 |
. . . . . . . . 9
⊢ ((𝐴 ∖ {𝑥}) ∩ {𝑥}) = ({𝑥} ∩ (𝐴 ∖ {𝑥})) |
52 | | disjdif 3992 |
. . . . . . . . 9
⊢ ({𝑥} ∩ (𝐴 ∖ {𝑥})) = ∅ |
53 | 51, 52 | eqtri 2632 |
. . . . . . . 8
⊢ ((𝐴 ∖ {𝑥}) ∩ {𝑥}) = ∅ |
54 | 53 | a1i 11 |
. . . . . . 7
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ∖ {𝑥}) ∩ {𝑥}) = ∅) |
55 | | cdaun 8877 |
. . . . . . 7
⊢ (((𝐴 ∖ {𝑥}) ∈ V ∧ {𝑥} ∈ V ∧ ((𝐴 ∖ {𝑥}) ∩ {𝑥}) = ∅) → ((𝐴 ∖ {𝑥}) +𝑐 {𝑥}) ≈ ((𝐴 ∖ {𝑥}) ∪ {𝑥})) |
56 | 36, 50, 54, 55 | syl3anc 1318 |
. . . . . 6
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ∖ {𝑥}) +𝑐 {𝑥}) ≈ ((𝐴 ∖ {𝑥}) ∪ {𝑥})) |
57 | 56, 34 | breqtrd 4609 |
. . . . 5
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ∖ {𝑥}) +𝑐 {𝑥}) ≈ 𝐴) |
58 | | pwen 8018 |
. . . . 5
⊢ (((𝐴 ∖ {𝑥}) +𝑐 {𝑥}) ≈ 𝐴 → 𝒫 ((𝐴 ∖ {𝑥}) +𝑐 {𝑥}) ≈ 𝒫 𝐴) |
59 | 57, 58 | syl 17 |
. . . 4
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝒫 ((𝐴 ∖ {𝑥}) +𝑐 {𝑥}) ≈ 𝒫 𝐴) |
60 | | domentr 7901 |
. . . 4
⊢ (((𝐴 × 2𝑜)
≼ 𝒫 ((𝐴
∖ {𝑥})
+𝑐 {𝑥})
∧ 𝒫 ((𝐴 ∖
{𝑥}) +𝑐
{𝑥}) ≈ 𝒫
𝐴) → (𝐴 × 2𝑜)
≼ 𝒫 𝐴) |
61 | 49, 59, 60 | syl2anc 691 |
. . 3
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 × 2𝑜) ≼
𝒫 𝐴) |
62 | 9, 61 | exlimddv 1850 |
. 2
⊢
(1𝑜 ≺ 𝐴 → (𝐴 × 2𝑜) ≼
𝒫 𝐴) |
63 | | domtr 7895 |
. 2
⊢ (((𝐴 +𝑐
2𝑜) ≼ (𝐴 × 2𝑜) ∧ (𝐴 × 2𝑜)
≼ 𝒫 𝐴) →
(𝐴 +𝑐
2𝑜) ≼ 𝒫 𝐴) |
64 | 3, 62, 63 | syl2anc 691 |
1
⊢
(1𝑜 ≺ 𝐴 → (𝐴 +𝑐
2𝑜) ≼ 𝒫 𝐴) |