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 = z → y ≺ x ↔ z ≺ x
6 pweq ⊢ y = z → 𝒫 y = 𝒫 z
7 6 breq2d ⊢ y = z → x ≺ 𝒫 y ↔ x ≺ 𝒫 z
8 5 7 anbi12d ⊢ y = z → y ≺ x ∧ x ≺ 𝒫 y ↔ z ≺ x ∧ x ≺ 𝒫 z
9 8 notbid ⊢ y = z → ¬ y ≺ x ∧ x ≺ 𝒫 y ↔ ¬ z ≺ x ∧ x ≺ 𝒫 z
10 9 albidv ⊢ y = z → ∀ x ¬ y ≺ x ∧ x ≺ 𝒫 y ↔ ∀ x ¬ z ≺ x ∧ x ≺ 𝒫 z
11 breq1 ⊢ z = A → z ≺ x ↔ A ≺ x
12 pweq ⊢ z = A → 𝒫 z = 𝒫 A
13 12 breq2d ⊢ z = A → x ≺ 𝒫 z ↔ x ≺ 𝒫 A
14 11 13 anbi12d ⊢ z = A → z ≺ x ∧ x ≺ 𝒫 z ↔ A ≺ x ∧ x ≺ 𝒫 A
15 14 notbid ⊢ z = A → ¬ z ≺ x ∧ x ≺ 𝒫 z ↔ ¬ A ≺ x ∧ x ≺ 𝒫 A
16 15 albidv ⊢ z = A → ∀ x ¬ z ≺ x ∧ x ≺ 𝒫 z ↔ ∀ x ¬ A ≺ x ∧ x ≺ 𝒫 A
17 10 16 elabgw ⊢ A ∈ V → A ∈ y | ∀ x ¬ y ≺ x ∧ x ≺ 𝒫 y ↔ ∀ x ¬ A ≺ x ∧ x ≺ 𝒫 A
18 17 orbi2d ⊢ A ∈ V → A ∈ Fin ∨ A ∈ y | ∀ x ¬ y ≺ x ∧ x ≺ 𝒫 y ↔ A ∈ Fin ∨ ∀ x ¬ A ≺ x ∧ x ≺ 𝒫 A
19 4 18 syl5bb ⊢ A ∈ V → A ∈ GCH ↔ A ∈ Fin ∨ ∀ x ¬ A ≺ x ∧ x ≺ 𝒫 A