Step | Hyp | Ref
| Expression |
1 | | 1sdom2 8719 |
. . 3
⊢
1o ≺ 2o |
2 | | djuxpdom 9613 |
. . 3
⊢
((1o ≺ 𝐴 ∧ 1o ≺ 2o)
→ (𝐴 ⊔
2o) ≼ (𝐴
× 2o)) |
3 | 1, 2 | mpan2 689 |
. 2
⊢
(1o ≺ 𝐴 → (𝐴 ⊔ 2o) ≼ (𝐴 ×
2o)) |
4 | | sdom0 8651 |
. . . . . 6
⊢ ¬
1o ≺ ∅ |
5 | | breq2 5072 |
. . . . . 6
⊢ (𝐴 = ∅ → (1o
≺ 𝐴 ↔
1o ≺ ∅)) |
6 | 4, 5 | mtbiri 329 |
. . . . 5
⊢ (𝐴 = ∅ → ¬
1o ≺ 𝐴) |
7 | 6 | con2i 141 |
. . . 4
⊢
(1o ≺ 𝐴 → ¬ 𝐴 = ∅) |
8 | | neq0 4311 |
. . . 4
⊢ (¬
𝐴 = ∅ ↔
∃𝑥 𝑥 ∈ 𝐴) |
9 | 7, 8 | sylib 220 |
. . 3
⊢
(1o ≺ 𝐴 → ∃𝑥 𝑥 ∈ 𝐴) |
10 | | relsdom 8518 |
. . . . . . . . . 10
⊢ Rel
≺ |
11 | 10 | brrelex2i 5611 |
. . . . . . . . 9
⊢
(1o ≺ 𝐴 → 𝐴 ∈ V) |
12 | 11 | adantr 483 |
. . . . . . . 8
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝐴 ∈ V) |
13 | | enrefg 8543 |
. . . . . . . 8
⊢ (𝐴 ∈ V → 𝐴 ≈ 𝐴) |
14 | 12, 13 | syl 17 |
. . . . . . 7
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝐴 ≈ 𝐴) |
15 | | df2o2 8120 |
. . . . . . . . 9
⊢
2o = {∅, {∅}} |
16 | | pwpw0 4748 |
. . . . . . . . 9
⊢ 𝒫
{∅} = {∅, {∅}} |
17 | 15, 16 | eqtr4i 2849 |
. . . . . . . 8
⊢
2o = 𝒫 {∅} |
18 | | 0ex 5213 |
. . . . . . . . . 10
⊢ ∅
∈ V |
19 | | vex 3499 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
20 | | en2sn 8595 |
. . . . . . . . . 10
⊢ ((∅
∈ V ∧ 𝑥 ∈ V)
→ {∅} ≈ {𝑥}) |
21 | 18, 19, 20 | mp2an 690 |
. . . . . . . . 9
⊢ {∅}
≈ {𝑥} |
22 | | pwen 8692 |
. . . . . . . . 9
⊢
({∅} ≈ {𝑥} → 𝒫 {∅} ≈
𝒫 {𝑥}) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . 8
⊢ 𝒫
{∅} ≈ 𝒫 {𝑥} |
24 | 17, 23 | eqbrtri 5089 |
. . . . . . 7
⊢
2o ≈ 𝒫 {𝑥} |
25 | | xpen 8682 |
. . . . . . 7
⊢ ((𝐴 ≈ 𝐴 ∧ 2o ≈ 𝒫
{𝑥}) → (𝐴 × 2o) ≈
(𝐴 × 𝒫 {𝑥})) |
26 | 14, 24, 25 | sylancl 588 |
. . . . . 6
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 × 2o) ≈ (𝐴 × 𝒫 {𝑥})) |
27 | | snex 5334 |
. . . . . . . 8
⊢ {𝑥} ∈ V |
28 | 27 | pwex 5283 |
. . . . . . 7
⊢ 𝒫
{𝑥} ∈
V |
29 | | uncom 4131 |
. . . . . . . . 9
⊢ ((𝐴 ∖ {𝑥}) ∪ {𝑥}) = ({𝑥} ∪ (𝐴 ∖ {𝑥})) |
30 | | simpr 487 |
. . . . . . . . . . 11
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
31 | 30 | snssd 4744 |
. . . . . . . . . 10
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → {𝑥} ⊆ 𝐴) |
32 | | undif 4432 |
. . . . . . . . . 10
⊢ ({𝑥} ⊆ 𝐴 ↔ ({𝑥} ∪ (𝐴 ∖ {𝑥})) = 𝐴) |
33 | 31, 32 | sylib 220 |
. . . . . . . . 9
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → ({𝑥} ∪ (𝐴 ∖ {𝑥})) = 𝐴) |
34 | 29, 33 | syl5eq 2870 |
. . . . . . . 8
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ∖ {𝑥}) ∪ {𝑥}) = 𝐴) |
35 | | difexg 5233 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (𝐴 ∖ {𝑥}) ∈ V) |
36 | 12, 35 | syl 17 |
. . . . . . . . 9
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) ∈ V) |
37 | | canth2g 8673 |
. . . . . . . . 9
⊢ ((𝐴 ∖ {𝑥}) ∈ V → (𝐴 ∖ {𝑥}) ≺ 𝒫 (𝐴 ∖ {𝑥})) |
38 | | domunsn 8669 |
. . . . . . . . 9
⊢ ((𝐴 ∖ {𝑥}) ≺ 𝒫 (𝐴 ∖ {𝑥}) → ((𝐴 ∖ {𝑥}) ∪ {𝑥}) ≼ 𝒫 (𝐴 ∖ {𝑥})) |
39 | 36, 37, 38 | 3syl 18 |
. . . . . . . 8
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ∖ {𝑥}) ∪ {𝑥}) ≼ 𝒫 (𝐴 ∖ {𝑥})) |
40 | 34, 39 | eqbrtrrd 5092 |
. . . . . . 7
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝐴 ≼ 𝒫 (𝐴 ∖ {𝑥})) |
41 | | xpdom1g 8616 |
. . . . . . 7
⊢
((𝒫 {𝑥}
∈ V ∧ 𝐴 ≼
𝒫 (𝐴 ∖ {𝑥})) → (𝐴 × 𝒫 {𝑥}) ≼ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) |
42 | 28, 40, 41 | sylancr 589 |
. . . . . 6
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 × 𝒫 {𝑥}) ≼ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) |
43 | | endomtr 8569 |
. . . . . 6
⊢ (((𝐴 × 2o) ≈
(𝐴 × 𝒫 {𝑥}) ∧ (𝐴 × 𝒫 {𝑥}) ≼ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) → (𝐴 × 2o) ≼ (𝒫
(𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) |
44 | 26, 42, 43 | syl2anc 586 |
. . . . 5
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 × 2o) ≼ (𝒫
(𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) |
45 | | pwdjuen 9609 |
. . . . . . 7
⊢ (((𝐴 ∖ {𝑥}) ∈ V ∧ {𝑥} ∈ V) → 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) |
46 | 36, 27, 45 | sylancl 588 |
. . . . . 6
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) |
47 | 46 | ensymd 8562 |
. . . . 5
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥}) ≈ 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥})) |
48 | | domentr 8570 |
. . . . 5
⊢ (((𝐴 × 2o) ≼
(𝒫 (𝐴 ∖
{𝑥}) × 𝒫
{𝑥}) ∧ (𝒫
(𝐴 ∖ {𝑥}) × 𝒫 {𝑥}) ≈ 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥})) → (𝐴 × 2o) ≼ 𝒫
((𝐴 ∖ {𝑥}) ⊔ {𝑥})) |
49 | 44, 47, 48 | syl2anc 586 |
. . . 4
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 × 2o) ≼ 𝒫
((𝐴 ∖ {𝑥}) ⊔ {𝑥})) |
50 | 27 | a1i 11 |
. . . . . . 7
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → {𝑥} ∈ V) |
51 | | incom 4180 |
. . . . . . . . 9
⊢ ((𝐴 ∖ {𝑥}) ∩ {𝑥}) = ({𝑥} ∩ (𝐴 ∖ {𝑥})) |
52 | | disjdif 4423 |
. . . . . . . . 9
⊢ ({𝑥} ∩ (𝐴 ∖ {𝑥})) = ∅ |
53 | 51, 52 | eqtri 2846 |
. . . . . . . 8
⊢ ((𝐴 ∖ {𝑥}) ∩ {𝑥}) = ∅ |
54 | 53 | a1i 11 |
. . . . . . 7
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ∖ {𝑥}) ∩ {𝑥}) = ∅) |
55 | | endjudisj 9596 |
. . . . . . 7
⊢ (((𝐴 ∖ {𝑥}) ∈ V ∧ {𝑥} ∈ V ∧ ((𝐴 ∖ {𝑥}) ∩ {𝑥}) = ∅) → ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ ((𝐴 ∖ {𝑥}) ∪ {𝑥})) |
56 | 36, 50, 54, 55 | syl3anc 1367 |
. . . . . 6
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ ((𝐴 ∖ {𝑥}) ∪ {𝑥})) |
57 | 56, 34 | breqtrd 5094 |
. . . . 5
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝐴) |
58 | | pwen 8692 |
. . . . 5
⊢ (((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝐴 → 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝒫 𝐴) |
59 | 57, 58 | syl 17 |
. . . 4
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝒫 𝐴) |
60 | | domentr 8570 |
. . . 4
⊢ (((𝐴 × 2o) ≼
𝒫 ((𝐴 ∖
{𝑥}) ⊔ {𝑥}) ∧ 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝒫 𝐴) → (𝐴 × 2o) ≼ 𝒫
𝐴) |
61 | 49, 59, 60 | syl2anc 586 |
. . 3
⊢
((1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 × 2o) ≼ 𝒫
𝐴) |
62 | 9, 61 | exlimddv 1936 |
. 2
⊢
(1o ≺ 𝐴 → (𝐴 × 2o) ≼ 𝒫
𝐴) |
63 | | domtr 8564 |
. 2
⊢ (((𝐴 ⊔ 2o) ≼
(𝐴 × 2o)
∧ (𝐴 ×
2o) ≼ 𝒫 𝐴) → (𝐴 ⊔ 2o) ≼ 𝒫
𝐴) |
64 | 3, 62, 63 | syl2anc 586 |
1
⊢
(1o ≺ 𝐴 → (𝐴 ⊔ 2o) ≼ 𝒫
𝐴) |