Definition df-ltfin 4442

Description: Define the less than relationship for finite cardinals. Definition from [Rosser] p. 527. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
df-ltfin	⊢ <fin = {x ∣ ∃m∃n(x = ⟪m, n⟫ ∧ (m ≠ ∅ ∧ ∃p ∈ Nn n = ((m +c p) +c 1c)))}

Distinct variable group:   m,n,p,x

Detailed syntax breakdown of Definition df-ltfin

Step	Hyp	Ref	Expression
1		cltfin 4434	. 2 class <fin
2		vx	. . . . . . . 8 setvar x
3	2	cv 1641	. . . . . . 7 class x
4		vm	. . . . . . . . 9 setvar m
5	4	cv 1641	. . . . . . . 8 class m
6		vn	. . . . . . . . 9 setvar n
7	6	cv 1641	. . . . . . . 8 class n
8	5, 7	copk 4058	. . . . . . 7 class ⟪m, n⟫
9	3, 8	wceq 1642	. . . . . 6 wff x = ⟪m, n⟫
10		c0 3551	. . . . . . . 8 class ∅
11	5, 10	wne 2517	. . . . . . 7 wff m ≠ ∅
12		vp	. . . . . . . . . . . 12 setvar p
13	12	cv 1641	. . . . . . . . . . 11 class p
14	5, 13	cplc 4376	. . . . . . . . . 10 class (m +c p)
15		c1c 4135	. . . . . . . . . 10 class 1c
16	14, 15	cplc 4376	. . . . . . . . 9 class ((m +c p) +c 1c)
17	7, 16	wceq 1642	. . . . . . . 8 wff n = ((m +c p) +c 1c)
18		cnnc 4374	. . . . . . . 8 class Nn
19	17, 12, 18	wrex 2616	. . . . . . 7 wff ∃p ∈ Nn n = ((m +c p) +c 1c)
20	11, 19	wa 358	. . . . . 6 wff (m ≠ ∅ ∧ ∃p ∈ Nn n = ((m +c p) +c 1c))
21	9, 20	wa 358	. . . . 5 wff (x = ⟪m, n⟫ ∧ (m ≠ ∅ ∧ ∃p ∈ Nn n = ((m +c p) +c 1c)))
22	21, 6	wex 1541	. . . 4 wff ∃n(x = ⟪m, n⟫ ∧ (m ≠ ∅ ∧ ∃p ∈ Nn n = ((m +c p) +c 1c)))
23	22, 4	wex 1541	. . 3 wff ∃m∃n(x = ⟪m, n⟫ ∧ (m ≠ ∅ ∧ ∃p ∈ Nn n = ((m +c p) +c 1c)))
24	23, 2	cab 2339	. 2 class {x ∣ ∃m∃n(x = ⟪m, n⟫ ∧ (m ≠ ∅ ∧ ∃p ∈ Nn n = ((m +c p) +c 1c)))}
25	1, 24	wceq 1642	1 wff <fin = {x ∣ ∃m∃n(x = ⟪m, n⟫ ∧ (m ≠ ∅ ∧ ∃p ∈ Nn n = ((m +c p) +c 1c)))}

This definition is referenced by:  opkltfing  4450  ltfinex  4465