Step |
Hyp |
Ref |
Expression |
1 |
|
dfuzi.1 |
⊢ 𝑁 ∈ ℤ |
2 |
|
ssintab |
⊢ ( { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ⊆ ∩ { 𝑥 ∣ ( 𝑁 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) } ↔ ∀ 𝑥 ( ( 𝑁 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) → { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ⊆ 𝑥 ) ) |
3 |
1
|
peano5uzi |
⊢ ( ( 𝑁 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) → { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ⊆ 𝑥 ) |
4 |
2 3
|
mpgbir |
⊢ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ⊆ ∩ { 𝑥 ∣ ( 𝑁 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) } |
5 |
1
|
zrei |
⊢ 𝑁 ∈ ℝ |
6 |
5
|
leidi |
⊢ 𝑁 ≤ 𝑁 |
7 |
|
breq2 |
⊢ ( 𝑧 = 𝑁 → ( 𝑁 ≤ 𝑧 ↔ 𝑁 ≤ 𝑁 ) ) |
8 |
7
|
elrab |
⊢ ( 𝑁 ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ↔ ( 𝑁 ∈ ℤ ∧ 𝑁 ≤ 𝑁 ) ) |
9 |
1 6 8
|
mpbir2an |
⊢ 𝑁 ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } |
10 |
|
peano2uz2 |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑦 ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ) → ( 𝑦 + 1 ) ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ) |
11 |
1 10
|
mpan |
⊢ ( 𝑦 ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } → ( 𝑦 + 1 ) ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ) |
12 |
11
|
rgen |
⊢ ∀ 𝑦 ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ( 𝑦 + 1 ) ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } |
13 |
|
zex |
⊢ ℤ ∈ V |
14 |
13
|
rabex |
⊢ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ∈ V |
15 |
|
eleq2 |
⊢ ( 𝑥 = { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } → ( 𝑁 ∈ 𝑥 ↔ 𝑁 ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ) ) |
16 |
|
eleq2 |
⊢ ( 𝑥 = { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } → ( ( 𝑦 + 1 ) ∈ 𝑥 ↔ ( 𝑦 + 1 ) ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ) ) |
17 |
16
|
raleqbi1dv |
⊢ ( 𝑥 = { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ↔ ∀ 𝑦 ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ( 𝑦 + 1 ) ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ) ) |
18 |
15 17
|
anbi12d |
⊢ ( 𝑥 = { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } → ( ( 𝑁 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) ↔ ( 𝑁 ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ∧ ∀ 𝑦 ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ( 𝑦 + 1 ) ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ) ) ) |
19 |
14 18
|
elab |
⊢ ( { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ∈ { 𝑥 ∣ ( 𝑁 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) } ↔ ( 𝑁 ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ∧ ∀ 𝑦 ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ( 𝑦 + 1 ) ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ) ) |
20 |
9 12 19
|
mpbir2an |
⊢ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ∈ { 𝑥 ∣ ( 𝑁 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) } |
21 |
|
intss1 |
⊢ ( { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ∈ { 𝑥 ∣ ( 𝑁 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) } → ∩ { 𝑥 ∣ ( 𝑁 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) } ⊆ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ) |
22 |
20 21
|
ax-mp |
⊢ ∩ { 𝑥 ∣ ( 𝑁 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) } ⊆ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } |
23 |
4 22
|
eqssi |
⊢ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } = ∩ { 𝑥 ∣ ( 𝑁 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) } |