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

Metamath Proof Explorer

Theorem pwdjudom

Description: A property of dominance over a powerset, and a main lemma for gchac . Similar to Lemma 2.3 of KanamoriPincus p. 420. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion pwdjudom ( 𝒫 ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ 𝐵 ) → 𝒫 𝐴 ≼ 𝐵 )

Proof

Step Hyp Ref Expression
1 canthwdom ⊢ ¬ 𝒫 𝐴 ≼* 𝐴
2 0ex ⊢ ∅ ∈ V
3 reldom ⊢ Rel ≼
4 3 brrelex2i ⊢ ( 𝒫 ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ 𝐵 ) → ( 𝐴 ⊔ 𝐵 ) ∈ V )
5 djuexb ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ( 𝐴 ⊔ 𝐵 ) ∈ V )
6 4 5 sylibr ⊢ ( 𝒫 ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
7 6 simpld ⊢ ( 𝒫 ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ 𝐵 ) → 𝐴 ∈ V )
8 xpsnen2g ⊢ ( ( ∅ ∈ V ∧ 𝐴 ∈ V ) → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
9 2 7 8 sylancr ⊢ ( 𝒫 ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ 𝐵 ) → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
10 endom ⊢ ( ( { ∅ } × 𝐴 ) ≈ 𝐴 → ( { ∅ } × 𝐴 ) ≼ 𝐴 )
11 domwdom ⊢ ( ( { ∅ } × 𝐴 ) ≼ 𝐴 → ( { ∅ } × 𝐴 ) ≼* 𝐴 )
12 wdomtr ⊢ ( ( 𝒫 𝐴 ≼* ( { ∅ } × 𝐴 ) ∧ ( { ∅ } × 𝐴 ) ≼* 𝐴 ) → 𝒫 𝐴 ≼* 𝐴 )
13 12 expcom ⊢ ( ( { ∅ } × 𝐴 ) ≼* 𝐴 → ( 𝒫 𝐴 ≼* ( { ∅ } × 𝐴 ) → 𝒫 𝐴 ≼* 𝐴 ) )
14 9 10 11 13 4syl ⊢ ( 𝒫 ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ 𝐵 ) → ( 𝒫 𝐴 ≼* ( { ∅ } × 𝐴 ) → 𝒫 𝐴 ≼* 𝐴 ) )
15 1 14 mtoi ⊢ ( 𝒫 ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ 𝐵 ) → ¬ 𝒫 𝐴 ≼* ( { ∅ } × 𝐴 ) )
16 pwdjuen ⊢ ( ( 𝐴 ∈ V ∧ 𝐴 ∈ V ) → 𝒫 ( 𝐴 ⊔ 𝐴 ) ≈ ( 𝒫 𝐴 × 𝒫 𝐴 ) )
17 7 7 16 syl2anc ⊢ ( 𝒫 ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ 𝐵 ) → 𝒫 ( 𝐴 ⊔ 𝐴 ) ≈ ( 𝒫 𝐴 × 𝒫 𝐴 ) )
18 domen1 ⊢ ( 𝒫 ( 𝐴 ⊔ 𝐴 ) ≈ ( 𝒫 𝐴 × 𝒫 𝐴 ) → ( 𝒫 ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ 𝐵 ) ↔ ( 𝒫 𝐴 × 𝒫 𝐴 ) ≼ ( 𝐴 ⊔ 𝐵 ) ) )
19 17 18 syl ⊢ ( 𝒫 ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ 𝐵 ) → ( 𝒫 ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ 𝐵 ) ↔ ( 𝒫 𝐴 × 𝒫 𝐴 ) ≼ ( 𝐴 ⊔ 𝐵 ) ) )
20 19 ibi ⊢ ( 𝒫 ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ 𝐵 ) → ( 𝒫 𝐴 × 𝒫 𝐴 ) ≼ ( 𝐴 ⊔ 𝐵 ) )
21 df-dju ⊢ ( 𝐴 ⊔ 𝐵 ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) )
22 20 21 breqtrdi ⊢ ( 𝒫 ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ 𝐵 ) → ( 𝒫 𝐴 × 𝒫 𝐴 ) ≼ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) )
23 unxpwdom ⊢ ( ( 𝒫 𝐴 × 𝒫 𝐴 ) ≼ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) → ( 𝒫 𝐴 ≼* ( { ∅ } × 𝐴 ) ∨ 𝒫 𝐴 ≼ ( { 1o } × 𝐵 ) ) )
24 22 23 syl ⊢ ( 𝒫 ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ 𝐵 ) → ( 𝒫 𝐴 ≼* ( { ∅ } × 𝐴 ) ∨ 𝒫 𝐴 ≼ ( { 1o } × 𝐵 ) ) )
25 24 ord ⊢ ( 𝒫 ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ 𝐵 ) → ( ¬ 𝒫 𝐴 ≼* ( { ∅ } × 𝐴 ) → 𝒫 𝐴 ≼ ( { 1o } × 𝐵 ) ) )
26 15 25 mpd ⊢ ( 𝒫 ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ 𝐵 ) → 𝒫 𝐴 ≼ ( { 1o } × 𝐵 ) )
27 1on ⊢ 1o ∈ On
28 6 simprd ⊢ ( 𝒫 ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ 𝐵 ) → 𝐵 ∈ V )
29 xpsnen2g ⊢ ( ( 1o ∈ On ∧ 𝐵 ∈ V ) → ( { 1o } × 𝐵 ) ≈ 𝐵 )
30 27 28 29 sylancr ⊢ ( 𝒫 ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ 𝐵 ) → ( { 1o } × 𝐵 ) ≈ 𝐵 )
31 domentr ⊢ ( ( 𝒫 𝐴 ≼ ( { 1o } × 𝐵 ) ∧ ( { 1o } × 𝐵 ) ≈ 𝐵 ) → 𝒫 𝐴 ≼ 𝐵 )
32 26 30 31 syl2anc ⊢ ( 𝒫 ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ 𝐵 ) → 𝒫 𝐴 ≼ 𝐵 )