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