gchdomtri

Description: Under certain conditions, a GCH-set can demonstrate trichotomy of dominance. Lemma for gchac . (Contributed by Mario Carneiro, 15-May-2015)

		Ref	Expression
	Assertion	gchdomtri	$⊢ (A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \to (A ≼ B \lor B ≼ A)$

Proof

Step	Hyp	Ref	Expression
1		sdomdom	$⊢ A ≺ B \to A ≼ B$
2	1	con3i	$⊢ \neg A ≼ B \to \neg A ≺ B$
3		reldom	$⊢ Rel ≼$
4	3	brrelex1i	$⊢ B ≼ 𝒫 A \to B \in V$
5	4	3ad2ant3	$⊢ (A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \to B \in V$
6		fidomtri2	$⊢ (B \in V \land A \in Fin) \to (B ≼ A \leftrightarrow \neg A ≺ B)$
7	5 6	sylan	$⊢ ((A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \land A \in Fin) \to (B ≼ A \leftrightarrow \neg A ≺ B)$
8	2 7	imbitrrid	$⊢ ((A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \land A \in Fin) \to (\neg A ≼ B \to B ≼ A)$
9	8	orrd	$⊢ ((A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \land A \in Fin) \to (A ≼ B \lor B ≼ A)$
10		simp1	$⊢ (A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \to A \in GCH$
11	10	adantr	$⊢ ((A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \land \neg A \in Fin) \to A \in GCH$
12		simpr	$⊢ ((A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \land \neg A \in Fin) \to \neg A \in Fin$
13		djudoml	$⊢ (A \in GCH \land B \in V) \to A ≼ (A ⊔︀ B)$
14	10 5 13	syl2anc	$⊢ (A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \to A ≼ (A ⊔︀ B)$
15	14	adantr	$⊢ ((A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \land \neg A \in Fin) \to A ≼ (A ⊔︀ B)$
16		djulepw	$⊢ ((A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \to (A ⊔︀ B) ≼ 𝒫 A$
17	16	3adant1	$⊢ (A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \to (A ⊔︀ B) ≼ 𝒫 A$
18	17	adantr	$⊢ ((A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \land \neg A \in Fin) \to (A ⊔︀ B) ≼ 𝒫 A$
19		gchor	$⊢ ((A \in GCH \land \neg A \in Fin) \land (A ≼ (A ⊔︀ B) \land (A ⊔︀ B) ≼ 𝒫 A)) \to (A \approx (A ⊔︀ B) \lor (A ⊔︀ B) \approx 𝒫 A)$
20	11 12 15 18 19	syl22anc	$⊢ ((A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \land \neg A \in Fin) \to (A \approx (A ⊔︀ B) \lor (A ⊔︀ B) \approx 𝒫 A)$
21		djudoml	$⊢ (B \in V \land A \in GCH) \to B ≼ (B ⊔︀ A)$
22	5 10 21	syl2anc	$⊢ (A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \to B ≼ (B ⊔︀ A)$
23		djucomen	$⊢ (B \in V \land A \in GCH) \to (B ⊔︀ A) \approx (A ⊔︀ B)$
24	5 10 23	syl2anc	$⊢ (A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \to (B ⊔︀ A) \approx (A ⊔︀ B)$
25		domentr	$⊢ (B ≼ (B ⊔︀ A) \land (B ⊔︀ A) \approx (A ⊔︀ B)) \to B ≼ (A ⊔︀ B)$
26	22 24 25	syl2anc	$⊢ (A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \to B ≼ (A ⊔︀ B)$
27		domen2	$⊢ A \approx (A ⊔︀ B) \to (B ≼ A \leftrightarrow B ≼ (A ⊔︀ B))$
28	26 27	syl5ibrcom	$⊢ (A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \to (A \approx (A ⊔︀ B) \to B ≼ A)$
29	28	imp	$⊢ ((A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \land A \approx (A ⊔︀ B)) \to B ≼ A$
30	29	olcd	$⊢ ((A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \land A \approx (A ⊔︀ B)) \to (A ≼ B \lor B ≼ A)$
31		simpl1	$⊢ ((A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \land (A ⊔︀ B) \approx 𝒫 A) \to A \in GCH$
32		canth2g	$⊢ A \in GCH \to A ≺ 𝒫 A$
33		sdomdom	$⊢ A ≺ 𝒫 A \to A ≼ 𝒫 A$
34	31 32 33	3syl	$⊢ ((A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \land (A ⊔︀ B) \approx 𝒫 A) \to A ≼ 𝒫 A$
35		simpl2	$⊢ ((A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \land (A ⊔︀ B) \approx 𝒫 A) \to (A ⊔︀ A) \approx A$
36		pwen	$⊢ (A ⊔︀ A) \approx A \to 𝒫 (A ⊔︀ A) \approx 𝒫 A$
37	35 36	syl	$⊢ ((A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \land (A ⊔︀ B) \approx 𝒫 A) \to 𝒫 (A ⊔︀ A) \approx 𝒫 A$
38		enen2	$⊢ (A ⊔︀ B) \approx 𝒫 A \to (𝒫 (A ⊔︀ A) \approx (A ⊔︀ B) \leftrightarrow 𝒫 (A ⊔︀ A) \approx 𝒫 A)$
39	38	adantl	$⊢ ((A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \land (A ⊔︀ B) \approx 𝒫 A) \to (𝒫 (A ⊔︀ A) \approx (A ⊔︀ B) \leftrightarrow 𝒫 (A ⊔︀ A) \approx 𝒫 A)$
40	37 39	mpbird	$⊢ ((A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \land (A ⊔︀ B) \approx 𝒫 A) \to 𝒫 (A ⊔︀ A) \approx (A ⊔︀ B)$
41		endom	$⊢ 𝒫 (A ⊔︀ A) \approx (A ⊔︀ B) \to 𝒫 (A ⊔︀ A) ≼ (A ⊔︀ B)$
42		pwdjudom	$⊢ 𝒫 (A ⊔︀ A) ≼ (A ⊔︀ B) \to 𝒫 A ≼ B$
43	40 41 42	3syl	$⊢ ((A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \land (A ⊔︀ B) \approx 𝒫 A) \to 𝒫 A ≼ B$
44		domtr	$⊢ (A ≼ 𝒫 A \land 𝒫 A ≼ B) \to A ≼ B$
45	34 43 44	syl2anc	$⊢ ((A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \land (A ⊔︀ B) \approx 𝒫 A) \to A ≼ B$
46	45	orcd	$⊢ ((A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \land (A ⊔︀ B) \approx 𝒫 A) \to (A ≼ B \lor B ≼ A)$
47	30 46	jaodan	$⊢ ((A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \land (A \approx (A ⊔︀ B) \lor (A ⊔︀ B) \approx 𝒫 A)) \to (A ≼ B \lor B ≼ A)$
48	20 47	syldan	$⊢ ((A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \land \neg A \in Fin) \to (A ≼ B \lor B ≼ A)$
49	9 48	pm2.61dan	$⊢ (A \in GCH \land (A ⊔︀ A) \approx A \land B ≼ 𝒫 A) \to (A ≼ B \lor B ≼ A)$

Metamath Proof Explorer

Theorem gchdomtri

Proof