Step |
Hyp |
Ref |
Expression |
1 |
|
relsdom |
⊢ Rel ≺ |
2 |
1
|
brrelex1i |
⊢ ( 𝐵 ≺ 𝒫 𝐴 → 𝐵 ∈ V ) |
3 |
2
|
adantl |
⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≺ 𝒫 𝐴 ) → 𝐵 ∈ V ) |
4 |
|
breq2 |
⊢ ( 𝑥 = 𝐵 → ( 𝐴 ≺ 𝑥 ↔ 𝐴 ≺ 𝐵 ) ) |
5 |
|
breq1 |
⊢ ( 𝑥 = 𝐵 → ( 𝑥 ≺ 𝒫 𝐴 ↔ 𝐵 ≺ 𝒫 𝐴 ) ) |
6 |
4 5
|
anbi12d |
⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ↔ ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≺ 𝒫 𝐴 ) ) ) |
7 |
6
|
spcegv |
⊢ ( 𝐵 ∈ V → ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≺ 𝒫 𝐴 ) → ∃ 𝑥 ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ) ) |
8 |
3 7
|
mpcom |
⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≺ 𝒫 𝐴 ) → ∃ 𝑥 ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ) |
9 |
|
df-ex |
⊢ ( ∃ 𝑥 ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ↔ ¬ ∀ 𝑥 ¬ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ) |
10 |
8 9
|
sylib |
⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≺ 𝒫 𝐴 ) → ¬ ∀ 𝑥 ¬ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ) |
11 |
|
elgch |
⊢ ( 𝐴 ∈ GCH → ( 𝐴 ∈ GCH ↔ ( 𝐴 ∈ Fin ∨ ∀ 𝑥 ¬ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ) ) ) |
12 |
11
|
ibi |
⊢ ( 𝐴 ∈ GCH → ( 𝐴 ∈ Fin ∨ ∀ 𝑥 ¬ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ) ) |
13 |
12
|
orcomd |
⊢ ( 𝐴 ∈ GCH → ( ∀ 𝑥 ¬ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ∨ 𝐴 ∈ Fin ) ) |
14 |
13
|
ord |
⊢ ( 𝐴 ∈ GCH → ( ¬ ∀ 𝑥 ¬ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) → 𝐴 ∈ Fin ) ) |
15 |
10 14
|
syl5 |
⊢ ( 𝐴 ∈ GCH → ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≺ 𝒫 𝐴 ) → 𝐴 ∈ Fin ) ) |
16 |
15
|
3impib |
⊢ ( ( 𝐴 ∈ GCH ∧ 𝐴 ≺ 𝐵 ∧ 𝐵 ≺ 𝒫 𝐴 ) → 𝐴 ∈ Fin ) |