New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > df-sfin | GIF version |
Description: Define the finite S relationship. This relationship encapsulates the idea of M being a "smaller" number than N. Definition from [Rosser] p. 530. (Contributed by SF, 12-Jan-2015.) |
Ref | Expression |
---|---|
df-sfin | ⊢ ( Sfin (M, N) ↔ (M ∈ Nn ∧ N ∈ Nn ∧ ∃a(℘1a ∈ M ∧ ℘a ∈ N))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cM | . . 3 class M | |
2 | cN | . . 3 class N | |
3 | 1, 2 | wsfin 4438 | . 2 wff Sfin (M, N) |
4 | cnnc 4373 | . . . 4 class Nn | |
5 | 1, 4 | wcel 1710 | . . 3 wff M ∈ Nn |
6 | 2, 4 | wcel 1710 | . . 3 wff N ∈ Nn |
7 | va | . . . . . . . 8 setvar a | |
8 | 7 | cv 1641 | . . . . . . 7 class a |
9 | 8 | cpw1 4135 | . . . . . 6 class ℘1a |
10 | 9, 1 | wcel 1710 | . . . . 5 wff ℘1a ∈ M |
11 | 8 | cpw 3722 | . . . . . 6 class ℘a |
12 | 11, 2 | wcel 1710 | . . . . 5 wff ℘a ∈ N |
13 | 10, 12 | wa 358 | . . . 4 wff (℘1a ∈ M ∧ ℘a ∈ N) |
14 | 13, 7 | wex 1541 | . . 3 wff ∃a(℘1a ∈ M ∧ ℘a ∈ N) |
15 | 5, 6, 14 | w3a 934 | . 2 wff (M ∈ Nn ∧ N ∈ Nn ∧ ∃a(℘1a ∈ M ∧ ℘a ∈ N)) |
16 | 3, 15 | wb 176 | 1 wff ( Sfin (M, N) ↔ (M ∈ Nn ∧ N ∈ Nn ∧ ∃a(℘1a ∈ M ∧ ℘a ∈ N))) |
Colors of variables: wff setvar class |
This definition is referenced by: srelk 4524 sfineq1 4526 sfineq2 4527 sfin01 4528 sfin112 4529 sfindbl 4530 sfintfin 4532 sfinltfin 4535 sfin111 4536 spfinsfincl 4539 vfinspnn 4541 1cvsfin 4542 vfinspsslem1 4550 |
Copyright terms: Public domain | W3C validator |