Step |
Hyp |
Ref |
Expression |
1 |
|
1sdom2 |
⊢ 1o ≺ 2o |
2 |
|
djuxpdom |
⊢ ( ( 1o ≺ 𝐴 ∧ 1o ≺ 2o ) → ( 𝐴 ⊔ 2o ) ≼ ( 𝐴 × 2o ) ) |
3 |
1 2
|
mpan2 |
⊢ ( 1o ≺ 𝐴 → ( 𝐴 ⊔ 2o ) ≼ ( 𝐴 × 2o ) ) |
4 |
|
sdom0 |
⊢ ¬ 1o ≺ ∅ |
5 |
|
breq2 |
⊢ ( 𝐴 = ∅ → ( 1o ≺ 𝐴 ↔ 1o ≺ ∅ ) ) |
6 |
4 5
|
mtbiri |
⊢ ( 𝐴 = ∅ → ¬ 1o ≺ 𝐴 ) |
7 |
6
|
con2i |
⊢ ( 1o ≺ 𝐴 → ¬ 𝐴 = ∅ ) |
8 |
|
neq0 |
⊢ ( ¬ 𝐴 = ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 ) |
9 |
7 8
|
sylib |
⊢ ( 1o ≺ 𝐴 → ∃ 𝑥 𝑥 ∈ 𝐴 ) |
10 |
|
relsdom |
⊢ Rel ≺ |
11 |
10
|
brrelex2i |
⊢ ( 1o ≺ 𝐴 → 𝐴 ∈ V ) |
12 |
11
|
adantr |
⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ∈ V ) |
13 |
|
enrefg |
⊢ ( 𝐴 ∈ V → 𝐴 ≈ 𝐴 ) |
14 |
12 13
|
syl |
⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ≈ 𝐴 ) |
15 |
|
df2o2 |
⊢ 2o = { ∅ , { ∅ } } |
16 |
|
pwpw0 |
⊢ 𝒫 { ∅ } = { ∅ , { ∅ } } |
17 |
15 16
|
eqtr4i |
⊢ 2o = 𝒫 { ∅ } |
18 |
|
0ex |
⊢ ∅ ∈ V |
19 |
|
vex |
⊢ 𝑥 ∈ V |
20 |
|
en2sn |
⊢ ( ( ∅ ∈ V ∧ 𝑥 ∈ V ) → { ∅ } ≈ { 𝑥 } ) |
21 |
18 19 20
|
mp2an |
⊢ { ∅ } ≈ { 𝑥 } |
22 |
|
pwen |
⊢ ( { ∅ } ≈ { 𝑥 } → 𝒫 { ∅ } ≈ 𝒫 { 𝑥 } ) |
23 |
21 22
|
ax-mp |
⊢ 𝒫 { ∅ } ≈ 𝒫 { 𝑥 } |
24 |
17 23
|
eqbrtri |
⊢ 2o ≈ 𝒫 { 𝑥 } |
25 |
|
xpen |
⊢ ( ( 𝐴 ≈ 𝐴 ∧ 2o ≈ 𝒫 { 𝑥 } ) → ( 𝐴 × 2o ) ≈ ( 𝐴 × 𝒫 { 𝑥 } ) ) |
26 |
14 24 25
|
sylancl |
⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 × 2o ) ≈ ( 𝐴 × 𝒫 { 𝑥 } ) ) |
27 |
|
snex |
⊢ { 𝑥 } ∈ V |
28 |
27
|
pwex |
⊢ 𝒫 { 𝑥 } ∈ V |
29 |
|
uncom |
⊢ ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) = ( { 𝑥 } ∪ ( 𝐴 ∖ { 𝑥 } ) ) |
30 |
|
simpr |
⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 ) |
31 |
30
|
snssd |
⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → { 𝑥 } ⊆ 𝐴 ) |
32 |
|
undif |
⊢ ( { 𝑥 } ⊆ 𝐴 ↔ ( { 𝑥 } ∪ ( 𝐴 ∖ { 𝑥 } ) ) = 𝐴 ) |
33 |
31 32
|
sylib |
⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( { 𝑥 } ∪ ( 𝐴 ∖ { 𝑥 } ) ) = 𝐴 ) |
34 |
29 33
|
syl5eq |
⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) = 𝐴 ) |
35 |
|
difexg |
⊢ ( 𝐴 ∈ V → ( 𝐴 ∖ { 𝑥 } ) ∈ V ) |
36 |
12 35
|
syl |
⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑥 } ) ∈ V ) |
37 |
|
canth2g |
⊢ ( ( 𝐴 ∖ { 𝑥 } ) ∈ V → ( 𝐴 ∖ { 𝑥 } ) ≺ 𝒫 ( 𝐴 ∖ { 𝑥 } ) ) |
38 |
|
domunsn |
⊢ ( ( 𝐴 ∖ { 𝑥 } ) ≺ 𝒫 ( 𝐴 ∖ { 𝑥 } ) → ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ≼ 𝒫 ( 𝐴 ∖ { 𝑥 } ) ) |
39 |
36 37 38
|
3syl |
⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ≼ 𝒫 ( 𝐴 ∖ { 𝑥 } ) ) |
40 |
34 39
|
eqbrtrrd |
⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ≼ 𝒫 ( 𝐴 ∖ { 𝑥 } ) ) |
41 |
|
xpdom1g |
⊢ ( ( 𝒫 { 𝑥 } ∈ V ∧ 𝐴 ≼ 𝒫 ( 𝐴 ∖ { 𝑥 } ) ) → ( 𝐴 × 𝒫 { 𝑥 } ) ≼ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) ) |
42 |
28 40 41
|
sylancr |
⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 × 𝒫 { 𝑥 } ) ≼ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) ) |
43 |
|
endomtr |
⊢ ( ( ( 𝐴 × 2o ) ≈ ( 𝐴 × 𝒫 { 𝑥 } ) ∧ ( 𝐴 × 𝒫 { 𝑥 } ) ≼ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) ) → ( 𝐴 × 2o ) ≼ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) ) |
44 |
26 42 43
|
syl2anc |
⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 × 2o ) ≼ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) ) |
45 |
|
pwdjuen |
⊢ ( ( ( 𝐴 ∖ { 𝑥 } ) ∈ V ∧ { 𝑥 } ∈ V ) → 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) ) |
46 |
36 27 45
|
sylancl |
⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) ) |
47 |
46
|
ensymd |
⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) ≈ 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ) |
48 |
|
domentr |
⊢ ( ( ( 𝐴 × 2o ) ≼ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) ∧ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) ≈ 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ) → ( 𝐴 × 2o ) ≼ 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ) |
49 |
44 47 48
|
syl2anc |
⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 × 2o ) ≼ 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ) |
50 |
27
|
a1i |
⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → { 𝑥 } ∈ V ) |
51 |
|
incom |
⊢ ( ( 𝐴 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ( { 𝑥 } ∩ ( 𝐴 ∖ { 𝑥 } ) ) |
52 |
|
disjdif |
⊢ ( { 𝑥 } ∩ ( 𝐴 ∖ { 𝑥 } ) ) = ∅ |
53 |
51 52
|
eqtri |
⊢ ( ( 𝐴 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ∅ |
54 |
53
|
a1i |
⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ∅ ) |
55 |
|
endjudisj |
⊢ ( ( ( 𝐴 ∖ { 𝑥 } ) ∈ V ∧ { 𝑥 } ∈ V ∧ ( ( 𝐴 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ∅ ) → ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) |
56 |
36 50 54 55
|
syl3anc |
⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) |
57 |
56 34
|
breqtrd |
⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ 𝐴 ) |
58 |
|
pwen |
⊢ ( ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ 𝐴 → 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ 𝒫 𝐴 ) |
59 |
57 58
|
syl |
⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ 𝒫 𝐴 ) |
60 |
|
domentr |
⊢ ( ( ( 𝐴 × 2o ) ≼ 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ∧ 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ 𝒫 𝐴 ) → ( 𝐴 × 2o ) ≼ 𝒫 𝐴 ) |
61 |
49 59 60
|
syl2anc |
⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 × 2o ) ≼ 𝒫 𝐴 ) |
62 |
9 61
|
exlimddv |
⊢ ( 1o ≺ 𝐴 → ( 𝐴 × 2o ) ≼ 𝒫 𝐴 ) |
63 |
|
domtr |
⊢ ( ( ( 𝐴 ⊔ 2o ) ≼ ( 𝐴 × 2o ) ∧ ( 𝐴 × 2o ) ≼ 𝒫 𝐴 ) → ( 𝐴 ⊔ 2o ) ≼ 𝒫 𝐴 ) |
64 |
3 62 63
|
syl2anc |
⊢ ( 1o ≺ 𝐴 → ( 𝐴 ⊔ 2o ) ≼ 𝒫 𝐴 ) |