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