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 |
|
breq1 |
⊢ ( 𝑧 = 𝐴 → ( 𝑧 ≺ 𝑥 ↔ 𝐴 ≺ 𝑥 ) ) |
12 |
|
pweq |
⊢ ( 𝑧 = 𝐴 → 𝒫 𝑧 = 𝒫 𝐴 ) |
13 |
12
|
breq2d |
⊢ ( 𝑧 = 𝐴 → ( 𝑥 ≺ 𝒫 𝑧 ↔ 𝑥 ≺ 𝒫 𝐴 ) ) |
14 |
11 13
|
anbi12d |
⊢ ( 𝑧 = 𝐴 → ( ( 𝑧 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝑧 ) ↔ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ) ) |
15 |
14
|
notbid |
⊢ ( 𝑧 = 𝐴 → ( ¬ ( 𝑧 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝑧 ) ↔ ¬ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ) ) |
16 |
15
|
albidv |
⊢ ( 𝑧 = 𝐴 → ( ∀ 𝑥 ¬ ( 𝑧 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝑧 ) ↔ ∀ 𝑥 ¬ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ) ) |
17 |
10 16
|
elabgw |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝑦 ∣ ∀ 𝑥 ¬ ( 𝑦 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝑦 ) } ↔ ∀ 𝑥 ¬ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ) ) |
18 |
17
|
orbi2d |
⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ∈ Fin ∨ 𝐴 ∈ { 𝑦 ∣ ∀ 𝑥 ¬ ( 𝑦 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝑦 ) } ) ↔ ( 𝐴 ∈ Fin ∨ ∀ 𝑥 ¬ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ) ) ) |
19 |
4 18
|
syl5bb |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ GCH ↔ ( 𝐴 ∈ Fin ∨ ∀ 𝑥 ¬ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ) ) ) |