This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem canthp1lem1

Description: Lemma for canthp1 . (Contributed by Mario Carneiro, 18-May-2015)

Ref Expression
Assertion canthp1lem1 ( 1o ≺ 𝐴 → ( 𝐴 ⊔ 2o ) ≼ 𝒫 𝐴 )

Proof

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 vsnex ⊢ { 𝑥 } ∈ V
28 27 pwex ⊢ 𝒫 { 𝑥 } ∈ V
29 uncom ⊢ ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) = ( { 𝑥 } ∪ ( 𝐴 ∖ { 𝑥 } ) )
30 simpr ⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
31 30 snssd ⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → { 𝑥 } ⊆ 𝐴 )
32 undif ⊢ ( { 𝑥 } ⊆ 𝐴 ↔ ( { 𝑥 } ∪ ( 𝐴 ∖ { 𝑥 } ) ) = 𝐴 )
33 31 32 sylib ⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( { 𝑥 } ∪ ( 𝐴 ∖ { 𝑥 } ) ) = 𝐴 )
34 29 33 eqtrid ⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) = 𝐴 )
35 12 difexd ⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑥 } ) ∈ V )
36 canth2g ⊢ ( ( 𝐴 ∖ { 𝑥 } ) ∈ V → ( 𝐴 ∖ { 𝑥 } ) ≺ 𝒫 ( 𝐴 ∖ { 𝑥 } ) )
37 domunsn ⊢ ( ( 𝐴 ∖ { 𝑥 } ) ≺ 𝒫 ( 𝐴 ∖ { 𝑥 } ) → ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ≼ 𝒫 ( 𝐴 ∖ { 𝑥 } ) )
38 35 36 37 3syl ⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ≼ 𝒫 ( 𝐴 ∖ { 𝑥 } ) )
39 34 38 eqbrtrrd ⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ≼ 𝒫 ( 𝐴 ∖ { 𝑥 } ) )
40 xpdom1g ⊢ ( ( 𝒫 { 𝑥 } ∈ V ∧ 𝐴 ≼ 𝒫 ( 𝐴 ∖ { 𝑥 } ) ) → ( 𝐴 × 𝒫 { 𝑥 } ) ≼ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) )
41 28 39 40 sylancr ⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 × 𝒫 { 𝑥 } ) ≼ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) )
42 endomtr ⊢ ( ( ( 𝐴 × 2o ) ≈ ( 𝐴 × 𝒫 { 𝑥 } ) ∧ ( 𝐴 × 𝒫 { 𝑥 } ) ≼ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) ) → ( 𝐴 × 2o ) ≼ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) )
43 26 41 42 syl2anc ⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 × 2o ) ≼ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) )
44 pwdjuen ⊢ ( ( ( 𝐴 ∖ { 𝑥 } ) ∈ V ∧ { 𝑥 } ∈ V ) → 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) )
45 35 27 44 sylancl ⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) )
46 45 ensymd ⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) ≈ 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) )
47 domentr ⊢ ( ( ( 𝐴 × 2o ) ≼ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) ∧ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) ≈ 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ) → ( 𝐴 × 2o ) ≼ 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) )
48 43 46 47 syl2anc ⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 × 2o ) ≼ 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) )
49 27 a1i ⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → { 𝑥 } ∈ V )
50 disjdifr ⊢ ( ( 𝐴 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ∅
51 50 a1i ⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ∅ )
52 endjudisj ⊢ ( ( ( 𝐴 ∖ { 𝑥 } ) ∈ V ∧ { 𝑥 } ∈ V ∧ ( ( 𝐴 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ∅ ) → ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) )
53 35 49 51 52 syl3anc ⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) )
54 53 34 breqtrd ⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ 𝐴 )
55 pwen ⊢ ( ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ 𝐴 → 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ 𝒫 𝐴 )
56 54 55 syl ⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ 𝒫 𝐴 )
57 domentr ⊢ ( ( ( 𝐴 × 2o ) ≼ 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ∧ 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ 𝒫 𝐴 ) → ( 𝐴 × 2o ) ≼ 𝒫 𝐴 )
58 48 56 57 syl2anc ⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 × 2o ) ≼ 𝒫 𝐴 )
59 9 58 exlimddv ⊢ ( 1o ≺ 𝐴 → ( 𝐴 × 2o ) ≼ 𝒫 𝐴 )
60 domtr ⊢ ( ( ( 𝐴 ⊔ 2o ) ≼ ( 𝐴 × 2o ) ∧ ( 𝐴 × 2o ) ≼ 𝒫 𝐴 ) → ( 𝐴 ⊔ 2o ) ≼ 𝒫 𝐴 )
61 3 59 60 syl2anc ⊢ ( 1o ≺ 𝐴 → ( 𝐴 ⊔ 2o ) ≼ 𝒫 𝐴 )