Step | Hyp | Ref
| Expression |
1 | | 1sdom2 8877 |
. . 3
⊢
1o ≺ 2o |
2 | | djuxpdom 9799 |
. . 3
⊢
((1o ≺ 𝐴 ∧ 1o ≺ 2o)
→ (𝐴 ⊔
2o) ≼ (𝐴
× 2o)) |
3 | 1, 2 | mpan2 691 |
. 2
⊢
(1o ≺ 𝐴 → (𝐴 ⊔ 2o) ≼ (𝐴 ×
2o)) |
4 | | sdom0 8778 |
. . . . . 6
⊢ ¬
1o ≺ ∅ |
5 | | breq2 5057 |
. . . . . 6
⊢ (𝐴 = ∅ → (1o
≺ 𝐴 ↔
1o ≺ ∅)) |
6 | 4, 5 | mtbiri 330 |
. . . . 5
⊢ (𝐴 = ∅ → ¬
1o ≺ 𝐴) |
7 | 6 | con2i 141 |
. . . 4
⊢
(1o ≺ 𝐴 → ¬ 𝐴 = ∅) |
8 | | neq0 4260 |
. . . 4
⊢ (¬
𝐴 = ∅ ↔
∃𝑥 𝑥 ∈ 𝐴) |
9 | 7, 8 | sylib 221 |
. . 3
⊢
(1o ≺ 𝐴 → ∃𝑥 𝑥 ∈ 𝐴) |
10 | | relsdom 8633 |
. . . . . . . . . 10
⊢ Rel
≺ |
11 | 10 | brrelex2i 5606 |
. . . . . . . . 9
⊢
(1o ≺ 𝐴 → 𝐴 ∈ V) |
12 | 11 | adantr 484 |
. . . . . . . 8
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝐴 ∈ V) |
13 | | enrefg 8660 |
. . . . . . . 8
⊢ (𝐴 ∈ V → 𝐴 ≈ 𝐴) |
14 | 12, 13 | syl 17 |
. . . . . . 7
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝐴 ≈ 𝐴) |
15 | | df2o2 8218 |
. . . . . . . . 9
⊢
2o = {∅, {∅}} |
16 | | pwpw0 4726 |
. . . . . . . . 9
⊢ 𝒫
{∅} = {∅, {∅}} |
17 | 15, 16 | eqtr4i 2768 |
. . . . . . . 8
⊢
2o = 𝒫 {∅} |
18 | | 0ex 5200 |
. . . . . . . . . 10
⊢ ∅
∈ V |
19 | | vex 3412 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
20 | | en2sn 8718 |
. . . . . . . . . 10
⊢ ((∅
∈ V ∧ 𝑥 ∈ V)
→ {∅} ≈ {𝑥}) |
21 | 18, 19, 20 | mp2an 692 |
. . . . . . . . 9
⊢ {∅}
≈ {𝑥} |
22 | | pwen 8819 |
. . . . . . . . 9
⊢
({∅} ≈ {𝑥} → 𝒫 {∅} ≈
𝒫 {𝑥}) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . 8
⊢ 𝒫
{∅} ≈ 𝒫 {𝑥} |
24 | 17, 23 | eqbrtri 5074 |
. . . . . . 7
⊢
2o ≈ 𝒫 {𝑥} |
25 | | xpen 8809 |
. . . . . . 7
⊢ ((𝐴 ≈ 𝐴 ∧ 2o ≈ 𝒫
{𝑥}) → (𝐴 × 2o) ≈
(𝐴 × 𝒫 {𝑥})) |
26 | 14, 24, 25 | sylancl 589 |
. . . . . 6
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 × 2o) ≈ (𝐴 × 𝒫 {𝑥})) |
27 | | snex 5324 |
. . . . . . . 8
⊢ {𝑥} ∈ V |
28 | 27 | pwex 5273 |
. . . . . . 7
⊢ 𝒫
{𝑥} ∈
V |
29 | | uncom 4067 |
. . . . . . . . 9
⊢ ((𝐴 ∖ {𝑥}) ∪ {𝑥}) = ({𝑥} ∪ (𝐴 ∖ {𝑥})) |
30 | | simpr 488 |
. . . . . . . . . . 11
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
31 | 30 | snssd 4722 |
. . . . . . . . . 10
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → {𝑥} ⊆ 𝐴) |
32 | | undif 4396 |
. . . . . . . . . 10
⊢ ({𝑥} ⊆ 𝐴 ↔ ({𝑥} ∪ (𝐴 ∖ {𝑥})) = 𝐴) |
33 | 31, 32 | sylib 221 |
. . . . . . . . 9
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → ({𝑥} ∪ (𝐴 ∖ {𝑥})) = 𝐴) |
34 | 29, 33 | eqtrid 2789 |
. . . . . . . 8
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ∖ {𝑥}) ∪ {𝑥}) = 𝐴) |
35 | 12 | difexd 5222 |
. . . . . . . . 9
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) ∈ V) |
36 | | canth2g 8800 |
. . . . . . . . 9
⊢ ((𝐴 ∖ {𝑥}) ∈ V → (𝐴 ∖ {𝑥}) ≺ 𝒫 (𝐴 ∖ {𝑥})) |
37 | | domunsn 8796 |
. . . . . . . . 9
⊢ ((𝐴 ∖ {𝑥}) ≺ 𝒫 (𝐴 ∖ {𝑥}) → ((𝐴 ∖ {𝑥}) ∪ {𝑥}) ≼ 𝒫 (𝐴 ∖ {𝑥})) |
38 | 35, 36, 37 | 3syl 18 |
. . . . . . . 8
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ∖ {𝑥}) ∪ {𝑥}) ≼ 𝒫 (𝐴 ∖ {𝑥})) |
39 | 34, 38 | eqbrtrrd 5077 |
. . . . . . 7
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝐴 ≼ 𝒫 (𝐴 ∖ {𝑥})) |
40 | | xpdom1g 8742 |
. . . . . . 7
⊢
((𝒫 {𝑥}
∈ V ∧ 𝐴 ≼
𝒫 (𝐴 ∖ {𝑥})) → (𝐴 × 𝒫 {𝑥}) ≼ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) |
41 | 28, 39, 40 | sylancr 590 |
. . . . . 6
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 × 𝒫 {𝑥}) ≼ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) |
42 | | endomtr 8686 |
. . . . . 6
⊢ (((𝐴 × 2o) ≈
(𝐴 × 𝒫 {𝑥}) ∧ (𝐴 × 𝒫 {𝑥}) ≼ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) → (𝐴 × 2o) ≼ (𝒫
(𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) |
43 | 26, 41, 42 | syl2anc 587 |
. . . . 5
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 × 2o) ≼ (𝒫
(𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) |
44 | | pwdjuen 9795 |
. . . . . . 7
⊢ (((𝐴 ∖ {𝑥}) ∈ V ∧ {𝑥} ∈ V) → 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) |
45 | 35, 27, 44 | sylancl 589 |
. . . . . 6
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) |
46 | 45 | ensymd 8679 |
. . . . 5
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥}) ≈ 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥})) |
47 | | domentr 8687 |
. . . . 5
⊢ (((𝐴 × 2o) ≼
(𝒫 (𝐴 ∖
{𝑥}) × 𝒫
{𝑥}) ∧ (𝒫
(𝐴 ∖ {𝑥}) × 𝒫 {𝑥}) ≈ 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥})) → (𝐴 × 2o) ≼ 𝒫
((𝐴 ∖ {𝑥}) ⊔ {𝑥})) |
48 | 43, 46, 47 | syl2anc 587 |
. . . 4
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 × 2o) ≼ 𝒫
((𝐴 ∖ {𝑥}) ⊔ {𝑥})) |
49 | 27 | a1i 11 |
. . . . . . 7
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → {𝑥} ∈ V) |
50 | | disjdifr 4387 |
. . . . . . . 8
⊢ ((𝐴 ∖ {𝑥}) ∩ {𝑥}) = ∅ |
51 | 50 | a1i 11 |
. . . . . . 7
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ∖ {𝑥}) ∩ {𝑥}) = ∅) |
52 | | endjudisj 9782 |
. . . . . . 7
⊢ (((𝐴 ∖ {𝑥}) ∈ V ∧ {𝑥} ∈ V ∧ ((𝐴 ∖ {𝑥}) ∩ {𝑥}) = ∅) → ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ ((𝐴 ∖ {𝑥}) ∪ {𝑥})) |
53 | 35, 49, 51, 52 | syl3anc 1373 |
. . . . . 6
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ ((𝐴 ∖ {𝑥}) ∪ {𝑥})) |
54 | 53, 34 | breqtrd 5079 |
. . . . 5
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝐴) |
55 | | pwen 8819 |
. . . . 5
⊢ (((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝐴 → 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝒫 𝐴) |
56 | 54, 55 | syl 17 |
. . . 4
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝒫 𝐴) |
57 | | domentr 8687 |
. . . 4
⊢ (((𝐴 × 2o) ≼
𝒫 ((𝐴 ∖
{𝑥}) ⊔ {𝑥}) ∧ 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝒫 𝐴) → (𝐴 × 2o) ≼ 𝒫
𝐴) |
58 | 48, 56, 57 | syl2anc 587 |
. . 3
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 × 2o) ≼ 𝒫
𝐴) |
59 | 9, 58 | exlimddv 1943 |
. 2
⊢
(1o ≺ 𝐴 → (𝐴 × 2o) ≼ 𝒫
𝐴) |
60 | | domtr 8681 |
. 2
⊢ (((𝐴 ⊔ 2o) ≼
(𝐴 × 2o)
∧ (𝐴 ×
2o) ≼ 𝒫 𝐴) → (𝐴 ⊔ 2o) ≼ 𝒫
𝐴) |
61 | 3, 59, 60 | syl2anc 587 |
1
⊢
(1o ≺ 𝐴 → (𝐴 ⊔ 2o) ≼ 𝒫
𝐴) |