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

Metamath Proof Explorer

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 bitrid ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ GCH ↔ ( 𝐴 ∈ Fin ∨ ∀ 𝑥 ¬ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ) ) )