Step |
Hyp |
Ref |
Expression |
1 |
|
uzsinds.1 |
⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) |
2 |
|
uzsinds.2 |
⊢ ( 𝑥 = 𝑁 → ( 𝜑 ↔ 𝜒 ) ) |
3 |
|
uzsinds.3 |
⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ∀ 𝑦 ∈ ( 𝑀 ... ( 𝑥 − 1 ) ) 𝜓 → 𝜑 ) ) |
4 |
|
ltweuz |
⊢ < We ( ℤ≥ ‘ 𝑀 ) |
5 |
|
fvex |
⊢ ( ℤ≥ ‘ 𝑀 ) ∈ V |
6 |
|
exse |
⊢ ( ( ℤ≥ ‘ 𝑀 ) ∈ V → < Se ( ℤ≥ ‘ 𝑀 ) ) |
7 |
5 6
|
ax-mp |
⊢ < Se ( ℤ≥ ‘ 𝑀 ) |
8 |
|
preduz |
⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) → Pred ( < , ( ℤ≥ ‘ 𝑀 ) , 𝑥 ) = ( 𝑀 ... ( 𝑥 − 1 ) ) ) |
9 |
8
|
raleqdv |
⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ∀ 𝑦 ∈ Pred ( < , ( ℤ≥ ‘ 𝑀 ) , 𝑥 ) 𝜓 ↔ ∀ 𝑦 ∈ ( 𝑀 ... ( 𝑥 − 1 ) ) 𝜓 ) ) |
10 |
9 3
|
sylbid |
⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ∀ 𝑦 ∈ Pred ( < , ( ℤ≥ ‘ 𝑀 ) , 𝑥 ) 𝜓 → 𝜑 ) ) |
11 |
4 7 1 2 10
|
wfis3 |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝜒 ) |