Metamath Proof Explorer


Theorem gchdju1

Description: An infinite GCH-set is idempotent under cardinal successor. (Contributed by Mario Carneiro, 18-May-2015)

Ref Expression
Assertion gchdju1 ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ⊔ 1o ) ≈ 𝐴 )

Proof

Step Hyp Ref Expression
1 1onn 1o ∈ ω
2 1 a1i ( ¬ 𝐴 ∈ Fin → 1o ∈ ω )
3 djudoml ( ( 𝐴 ∈ GCH ∧ 1o ∈ ω ) → 𝐴 ≼ ( 𝐴 ⊔ 1o ) )
4 2 3 sylan2 ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → 𝐴 ≼ ( 𝐴 ⊔ 1o ) )
5 simpr ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ¬ 𝐴 ∈ Fin )
6 nnfi ( 1o ∈ ω → 1o ∈ Fin )
7 1 6 mp1i ( ¬ 𝐴 ∈ Fin → 1o ∈ Fin )
8 fidomtri2 ( ( 𝐴 ∈ GCH ∧ 1o ∈ Fin ) → ( 𝐴 ≼ 1o ↔ ¬ 1o𝐴 ) )
9 7 8 sylan2 ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ≼ 1o ↔ ¬ 1o𝐴 ) )
10 1 6 mp1i ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → 1o ∈ Fin )
11 domfi ( ( 1o ∈ Fin ∧ 𝐴 ≼ 1o ) → 𝐴 ∈ Fin )
12 11 ex ( 1o ∈ Fin → ( 𝐴 ≼ 1o𝐴 ∈ Fin ) )
13 10 12 syl ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ≼ 1o𝐴 ∈ Fin ) )
14 9 13 sylbird ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( ¬ 1o𝐴𝐴 ∈ Fin ) )
15 5 14 mt3d ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → 1o𝐴 )
16 canthp1 ( 1o𝐴 → ( 𝐴 ⊔ 1o ) ≺ 𝒫 𝐴 )
17 15 16 syl ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ⊔ 1o ) ≺ 𝒫 𝐴 )
18 4 17 jca ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ≼ ( 𝐴 ⊔ 1o ) ∧ ( 𝐴 ⊔ 1o ) ≺ 𝒫 𝐴 ) )
19 gchen1 ( ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) ∧ ( 𝐴 ≼ ( 𝐴 ⊔ 1o ) ∧ ( 𝐴 ⊔ 1o ) ≺ 𝒫 𝐴 ) ) → 𝐴 ≈ ( 𝐴 ⊔ 1o ) )
20 18 19 mpdan ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → 𝐴 ≈ ( 𝐴 ⊔ 1o ) )
21 20 ensymd ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ⊔ 1o ) ≈ 𝐴 )