Step |
Hyp |
Ref |
Expression |
1 |
|
id |
⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 ) |
2 |
|
fveq2 |
⊢ ( 𝑥 = 𝑦 → ( ℵ ‘ 𝑥 ) = ( ℵ ‘ 𝑦 ) ) |
3 |
1 2
|
sseq12d |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ ( ℵ ‘ 𝑥 ) ↔ 𝑦 ⊆ ( ℵ ‘ 𝑦 ) ) ) |
4 |
|
id |
⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 ) |
5 |
|
fveq2 |
⊢ ( 𝑥 = 𝐴 → ( ℵ ‘ 𝑥 ) = ( ℵ ‘ 𝐴 ) ) |
6 |
4 5
|
sseq12d |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊆ ( ℵ ‘ 𝑥 ) ↔ 𝐴 ⊆ ( ℵ ‘ 𝐴 ) ) ) |
7 |
|
alephord2i |
⊢ ( 𝑥 ∈ On → ( 𝑦 ∈ 𝑥 → ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝑥 ) ) ) |
8 |
7
|
imp |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝑥 ) ) |
9 |
|
onelon |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ On ) |
10 |
|
alephon |
⊢ ( ℵ ‘ 𝑥 ) ∈ On |
11 |
|
ontr2 |
⊢ ( ( 𝑦 ∈ On ∧ ( ℵ ‘ 𝑥 ) ∈ On ) → ( ( 𝑦 ⊆ ( ℵ ‘ 𝑦 ) ∧ ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝑥 ) ) → 𝑦 ∈ ( ℵ ‘ 𝑥 ) ) ) |
12 |
9 10 11
|
sylancl |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑦 ⊆ ( ℵ ‘ 𝑦 ) ∧ ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝑥 ) ) → 𝑦 ∈ ( ℵ ‘ 𝑥 ) ) ) |
13 |
8 12
|
mpan2d |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( 𝑦 ⊆ ( ℵ ‘ 𝑦 ) → 𝑦 ∈ ( ℵ ‘ 𝑥 ) ) ) |
14 |
13
|
ralimdva |
⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 𝑦 ⊆ ( ℵ ‘ 𝑦 ) → ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ( ℵ ‘ 𝑥 ) ) ) |
15 |
10
|
onirri |
⊢ ¬ ( ℵ ‘ 𝑥 ) ∈ ( ℵ ‘ 𝑥 ) |
16 |
|
eleq1 |
⊢ ( 𝑦 = ( ℵ ‘ 𝑥 ) → ( 𝑦 ∈ ( ℵ ‘ 𝑥 ) ↔ ( ℵ ‘ 𝑥 ) ∈ ( ℵ ‘ 𝑥 ) ) ) |
17 |
16
|
rspccv |
⊢ ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ( ℵ ‘ 𝑥 ) → ( ( ℵ ‘ 𝑥 ) ∈ 𝑥 → ( ℵ ‘ 𝑥 ) ∈ ( ℵ ‘ 𝑥 ) ) ) |
18 |
15 17
|
mtoi |
⊢ ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ( ℵ ‘ 𝑥 ) → ¬ ( ℵ ‘ 𝑥 ) ∈ 𝑥 ) |
19 |
|
ontri1 |
⊢ ( ( 𝑥 ∈ On ∧ ( ℵ ‘ 𝑥 ) ∈ On ) → ( 𝑥 ⊆ ( ℵ ‘ 𝑥 ) ↔ ¬ ( ℵ ‘ 𝑥 ) ∈ 𝑥 ) ) |
20 |
10 19
|
mpan2 |
⊢ ( 𝑥 ∈ On → ( 𝑥 ⊆ ( ℵ ‘ 𝑥 ) ↔ ¬ ( ℵ ‘ 𝑥 ) ∈ 𝑥 ) ) |
21 |
18 20
|
syl5ibr |
⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ( ℵ ‘ 𝑥 ) → 𝑥 ⊆ ( ℵ ‘ 𝑥 ) ) ) |
22 |
14 21
|
syld |
⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 𝑦 ⊆ ( ℵ ‘ 𝑦 ) → 𝑥 ⊆ ( ℵ ‘ 𝑥 ) ) ) |
23 |
3 6 22
|
tfis3 |
⊢ ( 𝐴 ∈ On → 𝐴 ⊆ ( ℵ ‘ 𝐴 ) ) |