Step |
Hyp |
Ref |
Expression |
1 |
|
unblem.2 |
⊢ 𝐹 = ( rec ( ( 𝑥 ∈ V ↦ ∩ ( 𝐴 ∖ suc 𝑥 ) ) , ∩ 𝐴 ) ↾ ω ) |
2 |
|
omsson |
⊢ ω ⊆ On |
3 |
|
sstr |
⊢ ( ( 𝐴 ⊆ ω ∧ ω ⊆ On ) → 𝐴 ⊆ On ) |
4 |
2 3
|
mpan2 |
⊢ ( 𝐴 ⊆ ω → 𝐴 ⊆ On ) |
5 |
4
|
adantr |
⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → 𝐴 ⊆ On ) |
6 |
|
frfnom |
⊢ ( rec ( ( 𝑥 ∈ V ↦ ∩ ( 𝐴 ∖ suc 𝑥 ) ) , ∩ 𝐴 ) ↾ ω ) Fn ω |
7 |
1
|
fneq1i |
⊢ ( 𝐹 Fn ω ↔ ( rec ( ( 𝑥 ∈ V ↦ ∩ ( 𝐴 ∖ suc 𝑥 ) ) , ∩ 𝐴 ) ↾ ω ) Fn ω ) |
8 |
6 7
|
mpbir |
⊢ 𝐹 Fn ω |
9 |
1
|
unblem2 |
⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → ( 𝑧 ∈ ω → ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 ) ) |
10 |
9
|
ralrimiv |
⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → ∀ 𝑧 ∈ ω ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 ) |
11 |
|
ffnfv |
⊢ ( 𝐹 : ω ⟶ 𝐴 ↔ ( 𝐹 Fn ω ∧ ∀ 𝑧 ∈ ω ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 ) ) |
12 |
11
|
biimpri |
⊢ ( ( 𝐹 Fn ω ∧ ∀ 𝑧 ∈ ω ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 ) → 𝐹 : ω ⟶ 𝐴 ) |
13 |
8 10 12
|
sylancr |
⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → 𝐹 : ω ⟶ 𝐴 ) |
14 |
1
|
unblem3 |
⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → ( 𝑧 ∈ ω → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑧 ) ) ) |
15 |
14
|
ralrimiv |
⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → ∀ 𝑧 ∈ ω ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑧 ) ) |
16 |
|
omsmo |
⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑧 ∈ ω ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑧 ) ) → 𝐹 : ω –1-1→ 𝐴 ) |
17 |
5 13 15 16
|
syl21anc |
⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → 𝐹 : ω –1-1→ 𝐴 ) |