Step |
Hyp |
Ref |
Expression |
1 |
|
cfle |
⊢ ( cf ‘ ( cf ‘ 𝐴 ) ) ⊆ ( cf ‘ 𝐴 ) |
2 |
1
|
a1i |
⊢ ( 𝐴 ∈ On → ( cf ‘ ( cf ‘ 𝐴 ) ) ⊆ ( cf ‘ 𝐴 ) ) |
3 |
|
cfsmo |
⊢ ( 𝐴 ∈ On → ∃ 𝑓 ( 𝑓 : ( cf ‘ 𝐴 ) ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ( cf ‘ 𝐴 ) 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ) |
4 |
|
cfon |
⊢ ( cf ‘ 𝐴 ) ∈ On |
5 |
|
cfcoflem |
⊢ ( ( 𝐴 ∈ On ∧ ( cf ‘ 𝐴 ) ∈ On ) → ( ∃ 𝑓 ( 𝑓 : ( cf ‘ 𝐴 ) ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ( cf ‘ 𝐴 ) 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ( cf ‘ 𝐴 ) ⊆ ( cf ‘ ( cf ‘ 𝐴 ) ) ) ) |
6 |
4 5
|
mpan2 |
⊢ ( 𝐴 ∈ On → ( ∃ 𝑓 ( 𝑓 : ( cf ‘ 𝐴 ) ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ( cf ‘ 𝐴 ) 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ( cf ‘ 𝐴 ) ⊆ ( cf ‘ ( cf ‘ 𝐴 ) ) ) ) |
7 |
3 6
|
mpd |
⊢ ( 𝐴 ∈ On → ( cf ‘ 𝐴 ) ⊆ ( cf ‘ ( cf ‘ 𝐴 ) ) ) |
8 |
2 7
|
eqssd |
⊢ ( 𝐴 ∈ On → ( cf ‘ ( cf ‘ 𝐴 ) ) = ( cf ‘ 𝐴 ) ) |
9 |
|
cf0 |
⊢ ( cf ‘ ∅ ) = ∅ |
10 |
|
cff |
⊢ cf : On ⟶ On |
11 |
10
|
fdmi |
⊢ dom cf = On |
12 |
11
|
eleq2i |
⊢ ( 𝐴 ∈ dom cf ↔ 𝐴 ∈ On ) |
13 |
|
ndmfv |
⊢ ( ¬ 𝐴 ∈ dom cf → ( cf ‘ 𝐴 ) = ∅ ) |
14 |
12 13
|
sylnbir |
⊢ ( ¬ 𝐴 ∈ On → ( cf ‘ 𝐴 ) = ∅ ) |
15 |
14
|
fveq2d |
⊢ ( ¬ 𝐴 ∈ On → ( cf ‘ ( cf ‘ 𝐴 ) ) = ( cf ‘ ∅ ) ) |
16 |
9 15 14
|
3eqtr4a |
⊢ ( ¬ 𝐴 ∈ On → ( cf ‘ ( cf ‘ 𝐴 ) ) = ( cf ‘ 𝐴 ) ) |
17 |
8 16
|
pm2.61i |
⊢ ( cf ‘ ( cf ‘ 𝐴 ) ) = ( cf ‘ 𝐴 ) |