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

Metamath Proof Explorer

Theorem gchi

Description: The only GCH-sets which have other sets between it and its power set are finite sets. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion gchi ⊢ A ∈ GCH ∧ A ≺ B ∧ B ≺ 𝒫 A → A ∈ Fin

Proof

Step Hyp Ref Expression
1 relsdom ⊢ Rel ⁡ ≺
2 1 brrelex1i ⊢ B ≺ 𝒫 A → B ∈ V
3 2 adantl ⊢ A ≺ B ∧ B ≺ 𝒫 A → B ∈ V
4 breq2 ⊢ x = B → A ≺ x ↔ A ≺ B
5 breq1 ⊢ x = B → x ≺ 𝒫 A ↔ B ≺ 𝒫 A
6 4 5 anbi12d ⊢ x = B → A ≺ x ∧ x ≺ 𝒫 A ↔ A ≺ B ∧ B ≺ 𝒫 A
7 6 spcegv ⊢ B ∈ V → A ≺ B ∧ B ≺ 𝒫 A → ∃ x A ≺ x ∧ x ≺ 𝒫 A
8 3 7 mpcom ⊢ A ≺ B ∧ B ≺ 𝒫 A → ∃ x A ≺ x ∧ x ≺ 𝒫 A
9 df-ex ⊢ ∃ x A ≺ x ∧ x ≺ 𝒫 A ↔ ¬ ∀ x ¬ A ≺ x ∧ x ≺ 𝒫 A
10 8 9 sylib ⊢ A ≺ B ∧ B ≺ 𝒫 A → ¬ ∀ x ¬ A ≺ x ∧ x ≺ 𝒫 A
11 elgch ⊢ A ∈ GCH → A ∈ GCH ↔ A ∈ Fin ∨ ∀ x ¬ A ≺ x ∧ x ≺ 𝒫 A
12 11 ibi ⊢ A ∈ GCH → A ∈ Fin ∨ ∀ x ¬ A ≺ x ∧ x ≺ 𝒫 A
13 12 orcomd ⊢ A ∈ GCH → ∀ x ¬ A ≺ x ∧ x ≺ 𝒫 A ∨ A ∈ Fin
14 13 ord ⊢ A ∈ GCH → ¬ ∀ x ¬ A ≺ x ∧ x ≺ 𝒫 A → A ∈ Fin
15 10 14 syl5 ⊢ A ∈ GCH → A ≺ B ∧ B ≺ 𝒫 A → A ∈ Fin
16 15 3impib ⊢ A ∈ GCH ∧ A ≺ B ∧ B ≺ 𝒫 A → A ∈ Fin