Step | Hyp | Ref
| Expression |
1 | | 1sdom2 8563 |
. . 3
⊢
1o ≺ 2o |
2 | | djuxpdom 9457 |
. . 3
⊢
((1o ≺ 𝐴 ∧ 1o ≺ 2o)
→ (𝐴 ⊔
2o) ≼ (𝐴
× 2o)) |
3 | 1, 2 | mpan2 687 |
. 2
⊢
(1o ≺ 𝐴 → (𝐴 ⊔ 2o) ≼ (𝐴 ×
2o)) |
4 | | sdom0 8496 |
. . . . . 6
⊢ ¬
1o ≺ ∅ |
5 | | breq2 4966 |
. . . . . 6
⊢ (𝐴 = ∅ → (1o
≺ 𝐴 ↔
1o ≺ ∅)) |
6 | 4, 5 | mtbiri 328 |
. . . . 5
⊢ (𝐴 = ∅ → ¬
1o ≺ 𝐴) |
7 | 6 | con2i 141 |
. . . 4
⊢
(1o ≺ 𝐴 → ¬ 𝐴 = ∅) |
8 | | neq0 4229 |
. . . 4
⊢ (¬
𝐴 = ∅ ↔
∃𝑥 𝑥 ∈ 𝐴) |
9 | 7, 8 | sylib 219 |
. . 3
⊢
(1o ≺ 𝐴 → ∃𝑥 𝑥 ∈ 𝐴) |
10 | | relsdom 8364 |
. . . . . . . . . 10
⊢ Rel
≺ |
11 | 10 | brrelex2i 5495 |
. . . . . . . . 9
⊢
(1o ≺ 𝐴 → 𝐴 ∈ V) |
12 | 11 | adantr 481 |
. . . . . . . 8
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝐴 ∈ V) |
13 | | enrefg 8389 |
. . . . . . . 8
⊢ (𝐴 ∈ V → 𝐴 ≈ 𝐴) |
14 | 12, 13 | syl 17 |
. . . . . . 7
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝐴 ≈ 𝐴) |
15 | | df2o2 7969 |
. . . . . . . . 9
⊢
2o = {∅, {∅}} |
16 | | pwpw0 4653 |
. . . . . . . . 9
⊢ 𝒫
{∅} = {∅, {∅}} |
17 | 15, 16 | eqtr4i 2822 |
. . . . . . . 8
⊢
2o = 𝒫 {∅} |
18 | | 0ex 5102 |
. . . . . . . . . 10
⊢ ∅
∈ V |
19 | | vex 3440 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
20 | | en2sn 8441 |
. . . . . . . . . 10
⊢ ((∅
∈ V ∧ 𝑥 ∈ V)
→ {∅} ≈ {𝑥}) |
21 | 18, 19, 20 | mp2an 688 |
. . . . . . . . 9
⊢ {∅}
≈ {𝑥} |
22 | | pwen 8537 |
. . . . . . . . 9
⊢
({∅} ≈ {𝑥} → 𝒫 {∅} ≈
𝒫 {𝑥}) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . 8
⊢ 𝒫
{∅} ≈ 𝒫 {𝑥} |
24 | 17, 23 | eqbrtri 4983 |
. . . . . . 7
⊢
2o ≈ 𝒫 {𝑥} |
25 | | xpen 8527 |
. . . . . . 7
⊢ ((𝐴 ≈ 𝐴 ∧ 2o ≈ 𝒫
{𝑥}) → (𝐴 × 2o) ≈
(𝐴 × 𝒫 {𝑥})) |
26 | 14, 24, 25 | sylancl 586 |
. . . . . 6
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 × 2o) ≈ (𝐴 × 𝒫 {𝑥})) |
27 | | snex 5223 |
. . . . . . . 8
⊢ {𝑥} ∈ V |
28 | 27 | pwex 5172 |
. . . . . . 7
⊢ 𝒫
{𝑥} ∈
V |
29 | | uncom 4050 |
. . . . . . . . 9
⊢ ((𝐴 ∖ {𝑥}) ∪ {𝑥}) = ({𝑥} ∪ (𝐴 ∖ {𝑥})) |
30 | | simpr 485 |
. . . . . . . . . . 11
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
31 | 30 | snssd 4649 |
. . . . . . . . . 10
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → {𝑥} ⊆ 𝐴) |
32 | | undif 4344 |
. . . . . . . . . 10
⊢ ({𝑥} ⊆ 𝐴 ↔ ({𝑥} ∪ (𝐴 ∖ {𝑥})) = 𝐴) |
33 | 31, 32 | sylib 219 |
. . . . . . . . 9
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → ({𝑥} ∪ (𝐴 ∖ {𝑥})) = 𝐴) |
34 | 29, 33 | syl5eq 2843 |
. . . . . . . 8
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ∖ {𝑥}) ∪ {𝑥}) = 𝐴) |
35 | | difexg 5122 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (𝐴 ∖ {𝑥}) ∈ V) |
36 | 12, 35 | syl 17 |
. . . . . . . . 9
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) ∈ V) |
37 | | canth2g 8518 |
. . . . . . . . 9
⊢ ((𝐴 ∖ {𝑥}) ∈ V → (𝐴 ∖ {𝑥}) ≺ 𝒫 (𝐴 ∖ {𝑥})) |
38 | | domunsn 8514 |
. . . . . . . . 9
⊢ ((𝐴 ∖ {𝑥}) ≺ 𝒫 (𝐴 ∖ {𝑥}) → ((𝐴 ∖ {𝑥}) ∪ {𝑥}) ≼ 𝒫 (𝐴 ∖ {𝑥})) |
39 | 36, 37, 38 | 3syl 18 |
. . . . . . . 8
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ∖ {𝑥}) ∪ {𝑥}) ≼ 𝒫 (𝐴 ∖ {𝑥})) |
40 | 34, 39 | eqbrtrrd 4986 |
. . . . . . 7
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝐴 ≼ 𝒫 (𝐴 ∖ {𝑥})) |
41 | | xpdom1g 8461 |
. . . . . . 7
⊢
((𝒫 {𝑥}
∈ V ∧ 𝐴 ≼
𝒫 (𝐴 ∖ {𝑥})) → (𝐴 × 𝒫 {𝑥}) ≼ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) |
42 | 28, 40, 41 | sylancr 587 |
. . . . . 6
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 × 𝒫 {𝑥}) ≼ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) |
43 | | endomtr 8415 |
. . . . . 6
⊢ (((𝐴 × 2o) ≈
(𝐴 × 𝒫 {𝑥}) ∧ (𝐴 × 𝒫 {𝑥}) ≼ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) → (𝐴 × 2o) ≼ (𝒫
(𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) |
44 | 26, 42, 43 | syl2anc 584 |
. . . . 5
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 × 2o) ≼ (𝒫
(𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) |
45 | | pwdjuen 9453 |
. . . . . . 7
⊢ (((𝐴 ∖ {𝑥}) ∈ V ∧ {𝑥} ∈ V) → 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) |
46 | 36, 27, 45 | sylancl 586 |
. . . . . 6
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) |
47 | 46 | ensymd 8408 |
. . . . 5
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥}) ≈ 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥})) |
48 | | domentr 8416 |
. . . . 5
⊢ (((𝐴 × 2o) ≼
(𝒫 (𝐴 ∖
{𝑥}) × 𝒫
{𝑥}) ∧ (𝒫
(𝐴 ∖ {𝑥}) × 𝒫 {𝑥}) ≈ 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥})) → (𝐴 × 2o) ≼ 𝒫
((𝐴 ∖ {𝑥}) ⊔ {𝑥})) |
49 | 44, 47, 48 | syl2anc 584 |
. . . 4
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 × 2o) ≼ 𝒫
((𝐴 ∖ {𝑥}) ⊔ {𝑥})) |
50 | 27 | a1i 11 |
. . . . . . 7
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → {𝑥} ∈ V) |
51 | | incom 4099 |
. . . . . . . . 9
⊢ ((𝐴 ∖ {𝑥}) ∩ {𝑥}) = ({𝑥} ∩ (𝐴 ∖ {𝑥})) |
52 | | disjdif 4335 |
. . . . . . . . 9
⊢ ({𝑥} ∩ (𝐴 ∖ {𝑥})) = ∅ |
53 | 51, 52 | eqtri 2819 |
. . . . . . . 8
⊢ ((𝐴 ∖ {𝑥}) ∩ {𝑥}) = ∅ |
54 | 53 | a1i 11 |
. . . . . . 7
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ∖ {𝑥}) ∩ {𝑥}) = ∅) |
55 | | endjudisj 9440 |
. . . . . . 7
⊢ (((𝐴 ∖ {𝑥}) ∈ V ∧ {𝑥} ∈ V ∧ ((𝐴 ∖ {𝑥}) ∩ {𝑥}) = ∅) → ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ ((𝐴 ∖ {𝑥}) ∪ {𝑥})) |
56 | 36, 50, 54, 55 | syl3anc 1364 |
. . . . . 6
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ ((𝐴 ∖ {𝑥}) ∪ {𝑥})) |
57 | 56, 34 | breqtrd 4988 |
. . . . 5
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝐴) |
58 | | pwen 8537 |
. . . . 5
⊢ (((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝐴 → 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝒫 𝐴) |
59 | 57, 58 | syl 17 |
. . . 4
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝒫 𝐴) |
60 | | domentr 8416 |
. . . 4
⊢ (((𝐴 × 2o) ≼
𝒫 ((𝐴 ∖
{𝑥}) ⊔ {𝑥}) ∧ 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝒫 𝐴) → (𝐴 × 2o) ≼ 𝒫
𝐴) |
61 | 49, 59, 60 | syl2anc 584 |
. . 3
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 × 2o) ≼ 𝒫
𝐴) |
62 | 9, 61 | exlimddv 1913 |
. 2
⊢
(1o ≺ 𝐴 → (𝐴 × 2o) ≼ 𝒫
𝐴) |
63 | | domtr 8410 |
. 2
⊢ (((𝐴 ⊔ 2o) ≼
(𝐴 × 2o)
∧ (𝐴 ×
2o) ≼ 𝒫 𝐴) → (𝐴 ⊔ 2o) ≼ 𝒫
𝐴) |
64 | 3, 62, 63 | syl2anc 584 |
1
⊢
(1o ≺ 𝐴 → (𝐴 ⊔ 2o) ≼ 𝒫
𝐴) |