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	⊢ ( 𝜑 → ω ≼ 𝐴 )
	gchaclem.3	⊢ ( 𝜑 → 𝒫 𝐶 ∈ GCH )
	gchaclem.4	⊢ ( 𝜑 → ( 𝐴 ≼ 𝐶 ∧ ( 𝐵 ≼ 𝒫 𝐶 → 𝒫 𝐴 ≼ 𝐵 ) ) )
Assertion	gchaclem	⊢ ( 𝜑 → ( 𝐴 ≼ 𝒫 𝐶 ∧ ( 𝐵 ≼ 𝒫 𝒫 𝐶 → 𝒫 𝐴 ≼ 𝐵 ) ) )

Proof

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