Theorem finngch

Description: The exclusion of finite sets from consideration in df-gch is necessary, because otherwise finite sets larger than a singleton would violate the GCH property. (Contributed by Mario Carneiro, 10-Jun-2015)

	Ref	Expression
Assertion	finngch	⊢ ( ( 𝐴 ∈ Fin ∧ 1o ≺ 𝐴 ) → ( 𝐴 ≺ ( 𝐴 ⊔ 1o ) ∧ ( 𝐴 ⊔ 1o ) ≺ 𝒫 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		fin12	⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ FinII )
2		fin23	⊢ ( 𝐴 ∈ FinII → 𝐴 ∈ FinIII )
3		fin34	⊢ ( 𝐴 ∈ FinIII → 𝐴 ∈ FinIV )
4	1 2 3	3syl	⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ FinIV )
5		isfin4p1	⊢ ( 𝐴 ∈ FinIV ↔ 𝐴 ≺ ( 𝐴 ⊔ 1o ) )
6	4 5	sylib	⊢ ( 𝐴 ∈ Fin → 𝐴 ≺ ( 𝐴 ⊔ 1o ) )
7		canthp1	⊢ ( 1o ≺ 𝐴 → ( 𝐴 ⊔ 1o ) ≺ 𝒫 𝐴 )
8	6 7	anim12i	⊢ ( ( 𝐴 ∈ Fin ∧ 1o ≺ 𝐴 ) → ( 𝐴 ≺ ( 𝐴 ⊔ 1o ) ∧ ( 𝐴 ⊔ 1o ) ≺ 𝒫 𝐴 ) )