gchinf

Description: An infinite GCH-set is Dedekind-infinite. (Contributed by Mario Carneiro, 31-May-2015)

		Ref	Expression
	Assertion	gchinf	$⊢ (A \in GCH \land \neg A \in Fin) \to ω ≼ A$

Step	Hyp	Ref	Expression
1		gchdju1	$⊢ (A \in GCH \land \neg A \in Fin) \to (A ⊔︀ 1_{𝑜}) \approx A$
2	1	ensymd	$⊢ (A \in GCH \land \neg A \in Fin) \to A \approx (A ⊔︀ 1_{𝑜})$
3		isfin4-2	$⊢ A \in GCH \to (A \in {Fin}^{IV} \leftrightarrow \neg ω ≼ A)$
4	3	adantr	$⊢ (A \in GCH \land \neg A \in Fin) \to (A \in {Fin}^{IV} \leftrightarrow \neg ω ≼ A)$
5		isfin4p1	$⊢ A \in {Fin}^{IV} \leftrightarrow A ≺ (A ⊔︀ 1_{𝑜})$
6		sdomnen	$⊢ A ≺ (A ⊔︀ 1_{𝑜}) \to \neg A \approx (A ⊔︀ 1_{𝑜})$
7	5 6	sylbi	$⊢ A \in {Fin}^{IV} \to \neg A \approx (A ⊔︀ 1_{𝑜})$
8	4 7	syl6bir	$⊢ (A \in GCH \land \neg A \in Fin) \to (\neg ω ≼ A \to \neg A \approx (A ⊔︀ 1_{𝑜}))$
9	2 8	mt4d	$⊢ (A \in GCH \land \neg A \in Fin) \to ω ≼ A$

Metamath Proof Explorer