gchaclem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > gchaclem		Structured version Visualization version GIF version

Theorem gchaclem 9485

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

**Hypotheses**
Ref	Expression
gchaclem.1	⊢ (𝜑 → ω ≼ 𝐴)
gchaclem.3	⊢ (𝜑 → 𝒫 𝐶 ∈ GCH)
gchaclem.4	⊢ (𝜑 → (𝐴 ≼ 𝐶 ∧ (𝐵 ≼ 𝒫 𝐶 → 𝒫 𝐴 ≼ 𝐵)))

**Assertion**
Ref	Expression
gchaclem	⊢ (𝜑 → (𝐴 ≼ 𝒫 𝐶 ∧ (𝐵 ≼ 𝒫 𝒫 𝐶 → 𝒫 𝐴 ≼ 𝐵)))

**Proof of Theorem gchaclem**
Step	Hyp	Ref	Expression
1		gchaclem.4	. . . 4 ⊢ (𝜑 → (𝐴 ≼ 𝐶 ∧ (𝐵 ≼ 𝒫 𝐶 → 𝒫 𝐴 ≼ 𝐵)))
2	1	simpld 475	. . 3 ⊢ (𝜑 → 𝐴 ≼ 𝐶)
3		reldom 7946	. . . . . 6 ⊢ Rel ≼
4	3	brrelex2i 5149	. . . . 5 ⊢ (𝐴 ≼ 𝐶 → 𝐶 ∈ V)
5	2, 4	syl 17	. . . 4 ⊢ (𝜑 → 𝐶 ∈ V)
6		canth2g 8099	. . . 4 ⊢ (𝐶 ∈ V → 𝐶 ≺ 𝒫 𝐶)
7		sdomdom 7968	. . . 4 ⊢ (𝐶 ≺ 𝒫 𝐶 → 𝐶 ≼ 𝒫 𝐶)
8	5, 6, 7	3syl 18	. . 3 ⊢ (𝜑 → 𝐶 ≼ 𝒫 𝐶)
9		domtr 7994	. . 3 ⊢ ((𝐴 ≼ 𝐶 ∧ 𝐶 ≼ 𝒫 𝐶) → 𝐴 ≼ 𝒫 𝐶)
10	2, 8, 9	syl2anc 692	. 2 ⊢ (𝜑 → 𝐴 ≼ 𝒫 𝐶)
11		gchaclem.3	. . . . . 6 ⊢ (𝜑 → 𝒫 𝐶 ∈ GCH)
12	11	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 ≼ 𝒫 𝒫 𝐶) → 𝒫 𝐶 ∈ GCH)
13		gchaclem.1	. . . . . . . 8 ⊢ (𝜑 → ω ≼ 𝐴)
14		domtr 7994	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ≼ 𝐶) → ω ≼ 𝐶)
15	13, 2, 14	syl2anc 692	. . . . . . 7 ⊢ (𝜑 → ω ≼ 𝐶)
16	15	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 ≼ 𝒫 𝒫 𝐶) → ω ≼ 𝐶)
17		pwcdaidm 9002	. . . . . 6 ⊢ (ω ≼ 𝐶 → (𝒫 𝐶 +_𝑐 𝒫 𝐶) ≈ 𝒫 𝐶)
18	16, 17	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 ≼ 𝒫 𝒫 𝐶) → (𝒫 𝐶 +_𝑐 𝒫 𝐶) ≈ 𝒫 𝐶)
19		simpr 477	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 ≼ 𝒫 𝒫 𝐶) → 𝐵 ≼ 𝒫 𝒫 𝐶)
20		gchdomtri 9436	. . . . 5 ⊢ ((𝒫 𝐶 ∈ GCH ∧ (𝒫 𝐶 +_𝑐 𝒫 𝐶) ≈ 𝒫 𝐶 ∧ 𝐵 ≼ 𝒫 𝒫 𝐶) → (𝒫 𝐶 ≼ 𝐵 ∨ 𝐵 ≼ 𝒫 𝐶))
21	12, 18, 19, 20	syl3anc 1324	. . . 4 ⊢ ((𝜑 ∧ 𝐵 ≼ 𝒫 𝒫 𝐶) → (𝒫 𝐶 ≼ 𝐵 ∨ 𝐵 ≼ 𝒫 𝐶))
22	21	ex 450	. . 3 ⊢ (𝜑 → (𝐵 ≼ 𝒫 𝒫 𝐶 → (𝒫 𝐶 ≼ 𝐵 ∨ 𝐵 ≼ 𝒫 𝐶)))
23		pwdom 8097	. . . . 5 ⊢ (𝐴 ≼ 𝐶 → 𝒫 𝐴 ≼ 𝒫 𝐶)
24		domtr 7994	. . . . . 6 ⊢ ((𝒫 𝐴 ≼ 𝒫 𝐶 ∧ 𝒫 𝐶 ≼ 𝐵) → 𝒫 𝐴 ≼ 𝐵)
25	24	ex 450	. . . . 5 ⊢ (𝒫 𝐴 ≼ 𝒫 𝐶 → (𝒫 𝐶 ≼ 𝐵 → 𝒫 𝐴 ≼ 𝐵))
26	2, 23, 25	3syl 18	. . . 4 ⊢ (𝜑 → (𝒫 𝐶 ≼ 𝐵 → 𝒫 𝐴 ≼ 𝐵))
27	1	simprd 479	. . . 4 ⊢ (𝜑 → (𝐵 ≼ 𝒫 𝐶 → 𝒫 𝐴 ≼ 𝐵))
28	26, 27	jaod 395	. . 3 ⊢ (𝜑 → ((𝒫 𝐶 ≼ 𝐵 ∨ 𝐵 ≼ 𝒫 𝐶) → 𝒫 𝐴 ≼ 𝐵))
29	22, 28	syld 47	. 2 ⊢ (𝜑 → (𝐵 ≼ 𝒫 𝒫 𝐶 → 𝒫 𝐴 ≼ 𝐵))
30	10, 29	jca 554	1 ⊢ (𝜑 → (𝐴 ≼ 𝒫 𝐶 ∧ (𝐵 ≼ 𝒫 𝒫 𝐶 → 𝒫 𝐴 ≼ 𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∨ wo 383 ∧ wa 384 ∈ wcel 1988 Vcvv 3195 𝒫 cpw 4149 class class class wbr 4644 (class class class)co 6635 ωcom 7050 ≈ cen 7937 ≼ cdom 7938 ≺ csdm 7939 +_𝑐 ccda 8974 GCHcgch 9427

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1720 ax-4 1735 ax-5 1837 ax-6 1886 ax-7 1933 ax-8 1990 ax-9 1997 ax-10 2017 ax-11 2032 ax-12 2045 ax-13 2244 ax-ext 2600 ax-sep 4772 ax-nul 4780 ax-pow 4834 ax-pr 4897 ax-un 6934

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1037 df-3an 1038 df-tru 1484 df-ex 1703 df-nf 1708 df-sb 1879 df-eu 2472 df-mo 2473 df-clab 2607 df-cleq 2613 df-clel 2616 df-nfc 2751 df-ne 2792 df-ral 2914 df-rex 2915 df-reu 2916 df-rab 2918 df-v 3197 df-sbc 3430 df-csb 3527 df-dif 3570 df-un 3572 df-in 3574 df-ss 3581 df-pss 3583 df-nul 3908 df-if 4078 df-pw 4151 df-sn 4169 df-pr 4171 df-tp 4173 df-op 4175 df-uni 4428 df-int 4467 df-iun 4513 df-br 4645 df-opab 4704 df-mpt 4721 df-tr 4744 df-id 5014 df-eprel 5019 df-po 5025 df-so 5026 df-fr 5063 df-we 5065 df-xp 5110 df-rel 5111 df-cnv 5112 df-co 5113 df-dm 5114 df-rn 5115 df-res 5116 df-ima 5117 df-ord 5714 df-on 5715 df-lim 5716 df-suc 5717 df-iota 5839 df-fun 5878 df-fn 5879 df-f 5880 df-f1 5881 df-fo 5882 df-f1o 5883 df-fv 5884 df-ov 6638 df-oprab 6639 df-mpt2 6640 df-om 7051 df-1st 7153 df-2nd 7154 df-1o 7545 df-2o 7546 df-er 7727 df-map 7844 df-en 7941 df-dom 7942 df-sdom 7943 df-fin 7944 df-wdom 8449 df-card 8750 df-cda 8975 df-gch 9428

This theorem is referenced by: (None)

W3C validator