Metamath Proof Explorer

Theorem gchaclem

Description: Lemma for gchac (obsolete, used in Sierpiński's proof). (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Hypotheses gchaclem.1 ⊢φ→ω≼A
gchaclem.3 ⊢φ→𝒫C∈GCH
gchaclem.4 ⊢φ→A≼C∧B≼𝒫C→𝒫A≼B
Assertion gchaclem ⊢φ→A≼𝒫C∧B≼𝒫𝒫C→𝒫A≼B

Proof

Step Hyp Ref Expression
1 gchaclem.1 ⊢φ→ω≼A
2 gchaclem.3 ⊢φ→𝒫C∈GCH
3 gchaclem.4 ⊢φ→A≼C∧B≼𝒫C→𝒫A≼B
4 3 simpld ⊢φ→A≼C
5 reldom ⊢Rel⁡≼
6 5 brrelex2i ⊢A≼C→C∈V
7 4 6 syl ⊢φ→C∈V
8 canth2g ⊢C∈V→C≺𝒫C
9 sdomdom ⊢C≺𝒫C→C≼𝒫C
10 7 8 9 3syl ⊢φ→C≼𝒫C
11 domtr ⊢A≼C∧C≼𝒫C→A≼𝒫C
12 4 10 11 syl2anc ⊢φ→A≼𝒫C
13 2 adantr ⊢φ∧B≼𝒫𝒫C→𝒫C∈GCH
14 domtr ⊢ω≼A∧A≼C→ω≼C
15 1 4 14 syl2anc ⊢φ→ω≼C
16 15 adantr ⊢φ∧B≼𝒫𝒫C→ω≼C
17 pwdjuidm ⊢ω≼C→𝒫C⊔︀𝒫C≈𝒫C
18 16 17 syl ⊢φ∧B≼𝒫𝒫C→𝒫C⊔︀𝒫C≈𝒫C
19 simpr ⊢φ∧B≼𝒫𝒫C→B≼𝒫𝒫C
20 gchdomtri ⊢𝒫C∈GCH∧𝒫C⊔︀𝒫C≈𝒫C∧B≼𝒫𝒫C→𝒫C≼B∨B≼𝒫C
21 13 18 19 20 syl3anc ⊢φ∧B≼𝒫𝒫C→𝒫C≼B∨B≼𝒫C
22 21 ex ⊢φ→B≼𝒫𝒫C→𝒫C≼B∨B≼𝒫C
23 pwdom ⊢A≼C→𝒫A≼𝒫C
24 domtr ⊢𝒫A≼𝒫C∧𝒫C≼B→𝒫A≼B
25 24 ex ⊢𝒫A≼𝒫C→𝒫C≼B→𝒫A≼B
26 4 23 25 3syl ⊢φ→𝒫C≼B→𝒫A≼B
27 3 simprd ⊢φ→B≼𝒫C→𝒫A≼B
28 26 27 jaod ⊢φ→𝒫C≼B∨B≼𝒫C→𝒫A≼B
29 22 28 syld ⊢φ→B≼𝒫𝒫C→𝒫A≼B
30 12 29 jca ⊢φ→A≼𝒫C∧B≼𝒫𝒫C→𝒫A≼B