Theorem elgch

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

	Ref	Expression
Assertion	elgch	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ GCH ↔ ( 𝐴 ∈ Fin ∨ ∀ 𝑥 ¬ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-gch	⊢ GCH = ( Fin ∪ { 𝑦 ∣ ∀ 𝑥 ¬ ( 𝑦 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝑦 ) } )
2	1	eleq2i	⊢ ( 𝐴 ∈ GCH ↔ 𝐴 ∈ ( Fin ∪ { 𝑦 ∣ ∀ 𝑥 ¬ ( 𝑦 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝑦 ) } ) )
3		elun	⊢ ( 𝐴 ∈ ( Fin ∪ { 𝑦 ∣ ∀ 𝑥 ¬ ( 𝑦 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝑦 ) } ) ↔ ( 𝐴 ∈ Fin ∨ 𝐴 ∈ { 𝑦 ∣ ∀ 𝑥 ¬ ( 𝑦 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝑦 ) } ) )
4	2 3	bitri	⊢ ( 𝐴 ∈ GCH ↔ ( 𝐴 ∈ Fin ∨ 𝐴 ∈ { 𝑦 ∣ ∀ 𝑥 ¬ ( 𝑦 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝑦 ) } ) )
5		breq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ≺ 𝑥 ↔ 𝐴 ≺ 𝑥 ) )
6		pweq	⊢ ( 𝑦 = 𝐴 → 𝒫 𝑦 = 𝒫 𝐴 )
7	6	breq2d	⊢ ( 𝑦 = 𝐴 → ( 𝑥 ≺ 𝒫 𝑦 ↔ 𝑥 ≺ 𝒫 𝐴 ) )
8	5 7	anbi12d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝑦 ) ↔ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ) )
9	8	notbid	⊢ ( 𝑦 = 𝐴 → ( ¬ ( 𝑦 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝑦 ) ↔ ¬ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ) )
10	9	albidv	⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ¬ ( 𝑦 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝑦 ) ↔ ∀ 𝑥 ¬ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ) )
11	10	elabg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝑦 ∣ ∀ 𝑥 ¬ ( 𝑦 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝑦 ) } ↔ ∀ 𝑥 ¬ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ) )
12	11	orbi2d	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ∈ Fin ∨ 𝐴 ∈ { 𝑦 ∣ ∀ 𝑥 ¬ ( 𝑦 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝑦 ) } ) ↔ ( 𝐴 ∈ Fin ∨ ∀ 𝑥 ¬ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ) ) )
13	4 12	syl5bb	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ GCH ↔ ( 𝐴 ∈ Fin ∨ ∀ 𝑥 ¬ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ) ) )