Metamath Proof Explorer

Theorem engch

Description: The property of being a GCH-set is a cardinal invariant. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion engch ⊢ A ≈ B → A ∈ GCH ↔ B ∈ GCH

Proof

Step Hyp Ref Expression
1 enfi ⊢ A ≈ B → A ∈ Fin ↔ B ∈ Fin
2 sdomen1 ⊢ A ≈ B → A ≺ x ↔ B ≺ x
3 pwen ⊢ A ≈ B → 𝒫 A ≈ 𝒫 B
4 sdomen2 ⊢ 𝒫 A ≈ 𝒫 B → x ≺ 𝒫 A ↔ x ≺ 𝒫 B
5 3 4 syl ⊢ A ≈ B → x ≺ 𝒫 A ↔ x ≺ 𝒫 B
6 2 5 anbi12d ⊢ A ≈ B → A ≺ x ∧ x ≺ 𝒫 A ↔ B ≺ x ∧ x ≺ 𝒫 B
7 6 notbid ⊢ A ≈ B → ¬ A ≺ x ∧ x ≺ 𝒫 A ↔ ¬ B ≺ x ∧ x ≺ 𝒫 B
8 7 albidv ⊢ A ≈ B → ∀ x ¬ A ≺ x ∧ x ≺ 𝒫 A ↔ ∀ x ¬ B ≺ x ∧ x ≺ 𝒫 B
9 1 8 orbi12d ⊢ A ≈ B → A ∈ Fin ∨ ∀ x ¬ A ≺ x ∧ x ≺ 𝒫 A ↔ B ∈ Fin ∨ ∀ x ¬ B ≺ x ∧ x ≺ 𝒫 B
10 relen ⊢ Rel ⁡ ≈
11 10 brrelex1i ⊢ A ≈ B → A ∈ V
12 elgch ⊢ A ∈ V → A ∈ GCH ↔ A ∈ Fin ∨ ∀ x ¬ A ≺ x ∧ x ≺ 𝒫 A
13 11 12 syl ⊢ A ≈ B → A ∈ GCH ↔ A ∈ Fin ∨ ∀ x ¬ A ≺ x ∧ x ≺ 𝒫 A
14 10 brrelex2i ⊢ A ≈ B → B ∈ V
15 elgch ⊢ B ∈ V → B ∈ GCH ↔ B ∈ Fin ∨ ∀ x ¬ B ≺ x ∧ x ≺ 𝒫 B
16 14 15 syl ⊢ A ≈ B → B ∈ GCH ↔ B ∈ Fin ∨ ∀ x ¬ B ≺ x ∧ x ≺ 𝒫 B
17 9 13 16 3bitr4d ⊢ A ≈ B → A ∈ GCH ↔ B ∈ GCH