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

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 ) ≈ 𝐴 )