Theorem gchinf

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

	Ref	Expression
Assertion	gchinf	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ω ≼ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		gchdju1	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ⊔ 1o ) ≈ 𝐴 )
2	1	ensymd	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → 𝐴 ≈ ( 𝐴 ⊔ 1o ) )
3		isfin4-2	⊢ ( 𝐴 ∈ GCH → ( 𝐴 ∈ FinIV ↔ ¬ ω ≼ 𝐴 ) )
4	3	adantr	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ∈ FinIV ↔ ¬ ω ≼ 𝐴 ) )
5		isfin4p1	⊢ ( 𝐴 ∈ FinIV ↔ 𝐴 ≺ ( 𝐴 ⊔ 1o ) )
6		sdomnen	⊢ ( 𝐴 ≺ ( 𝐴 ⊔ 1o ) → ¬ 𝐴 ≈ ( 𝐴 ⊔ 1o ) )
7	5 6	sylbi	⊢ ( 𝐴 ∈ FinIV → ¬ 𝐴 ≈ ( 𝐴 ⊔ 1o ) )
8	4 7	biimtrrdi	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( ¬ ω ≼ 𝐴 → ¬ 𝐴 ≈ ( 𝐴 ⊔ 1o ) ) )
9	2 8	mt4d	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ω ≼ 𝐴 )