Metamath Proof Explorer

Theorem elgch

Description: Elementhood in the collection of GCH-sets. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion elgch ⊢ A ∈ V → A ∈ GCH ↔ A ∈ Fin ∨ ∀ x ¬ A ≺ x ∧ x ≺ 𝒫 A

Proof

Step Hyp Ref Expression
1 df-gch ⊢ GCH = Fin ∪ y | ∀ x ¬ y ≺ x ∧ x ≺ 𝒫 y
2 1 eleq2i ⊢ A ∈ GCH ↔ A ∈ Fin ∪ y | ∀ x ¬ y ≺ x ∧ x ≺ 𝒫 y
3 elun ⊢ A ∈ Fin ∪ y | ∀ x ¬ y ≺ x ∧ x ≺ 𝒫 y ↔ A ∈ Fin ∨ A ∈ y | ∀ x ¬ y ≺ x ∧ x ≺ 𝒫 y
4 2 3 bitri ⊢ A ∈ GCH ↔ A ∈ Fin ∨ A ∈ y | ∀ x ¬ y ≺ x ∧ x ≺ 𝒫 y
5 breq1 ⊢ y = A → y ≺ x ↔ A ≺ x
6 pweq ⊢ y = A → 𝒫 y = 𝒫 A
7 6 breq2d ⊢ y = A → x ≺ 𝒫 y ↔ x ≺ 𝒫 A
8 5 7 anbi12d ⊢ y = A → y ≺ x ∧ x ≺ 𝒫 y ↔ A ≺ x ∧ x ≺ 𝒫 A
9 8 notbid ⊢ y = A → ¬ y ≺ x ∧ x ≺ 𝒫 y ↔ ¬ A ≺ x ∧ x ≺ 𝒫 A
10 9 albidv ⊢ y = A → ∀ x ¬ y ≺ x ∧ x ≺ 𝒫 y ↔ ∀ x ¬ A ≺ x ∧ x ≺ 𝒫 A
11 10 elabg ⊢ A ∈ V → A ∈ y | ∀ x ¬ y ≺ x ∧ x ≺ 𝒫 y ↔ ∀ x ¬ A ≺ x ∧ x ≺ 𝒫 A
12 11 orbi2d ⊢ A ∈ V → A ∈ Fin ∨ A ∈ y | ∀ x ¬ y ≺ x ∧ x ≺ 𝒫 y ↔ A ∈ Fin ∨ ∀ x ¬ A ≺ x ∧ x ≺ 𝒫 A
13 4 12 bitrid ⊢ A ∈ V → A ∈ GCH ↔ A ∈ Fin ∨ ∀ x ¬ A ≺ x ∧ x ≺ 𝒫 A