This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) → ω ≼ 𝐴 )