Theorem pssnn 3428

Description: A proper subset of a natural number is equinumerous to some smaller number. Lemma 6F of [Enderton] p. 137.

Assertion

Ref	Expression
pssnn	|- ((A e. om /\ B (. A) -> E.x e. A B ~~ x)

Distinct variable group(s):   x,A   x,B

Proof of Theorem pssnn

Step	Hyp	Ref	Expression
1		ssexg 1702	. . . . . 6 |- (A e. om -> (B (_ A -> B e. V))
2		pssss 1567	. . . . . 6 |- (B (. A -> B (_ A)
3	1, 2	syl5 22	. . . . 5 |- (A e. om -> (B (. A -> B e. V))
4		psseq1 1559	. . . . . . . 8 |- (w = B -> (w (. A <-> B (. A))
5		breq1 2065	. . . . . . . . 9 |- (w = B -> (w ~~ x <-> B ~~ x))
6	5	birexdv 1220	. . . . . . . 8 |- (w = B -> (E.x e. A w ~~ x <-> E.x e. A B ~~ x))
7	4, 6	imbi12d 474	. . . . . . 7 |- (w = B -> ((w (. A -> E.x e. A w ~~ x) <-> (B (. A -> E.x e. A B ~~ x)))
8	7	cla4gv 1396	. . . . . 6 |- (B e. V -> (A.w(w (. A -> E.x e. A w ~~ x) -> (B (. A -> E.x e. A B ~~ x)))
9		psseq2 1560	. . . . . . . . 9 |- (z = (/) -> (w (. z <-> w (. (/)))
10		rexeq 1325	. . . . . . . . 9 |- (z = (/) -> (E.x e. z w ~~ x <-> E.x e. (/) w ~~ x))
11	9, 10	imbi12d 474	. . . . . . . 8 |- (z = (/) -> ((w (. z -> E.x e. z w ~~ x) <-> (w (. (/) -> E.x e. (/) w ~~ x)))
12	11	bialdv 935	. . . . . . 7 |- (z = (/) -> (A.w(w (. z -> E.x e. z w ~~ x) <-> A.w(w (. (/) -> E.x e. (/) w ~~ x)))
13		psseq2 1560	. . . . . . . . 9 |- (z = y -> (w (. z <-> w (. y))
14		rexeq 1325	. . . . . . . . 9 |- (z = y -> (E.x e. z w ~~ x <-> E.x e. y w ~~ x))
15	13, 14	imbi12d 474	. . . . . . . 8 |- (z = y -> ((w (. z -> E.x e. z w ~~ x) <-> (w (. y -> E.x e. y w ~~ x)))
16	15	bialdv 935	. . . . . . 7 |- (z = y -> (A.w(w (. z -> E.x e. z w ~~ x) <-> A.w(w (. y -> E.x e. y w ~~ x)))
17		psseq2 1560	. . . . . . . . 9 |- (z = suc y -> (w (. z <-> w (. suc y))
18		rexeq 1325	. . . . . . . . 9 |- (z = suc y -> (E.x e. z w ~~ x <-> E.x e. suc yw ~~ x))
19	17, 18	imbi12d 474	. . . . . . . 8 |- (z = suc y -> ((w (. z -> E.x e. z w ~~ x) <-> (w (. suc y -> E.x e. suc yw ~~ x)))
20	19	bialdv 935	. . . . . . 7 |- (z = suc y -> (A.w(w (. z -> E.x e. z w ~~ x) <-> A.w(w (. suc y -> E.x e. suc yw ~~ x)))
21		psseq2 1560	. . . . . . . . 9 |- (z = A -> (w (. z <-> w (. A))
22		rexeq 1325	. . . . . . . . 9 |- (z = A -> (E.x e. z w ~~ x <-> E.x e. A w ~~ x))
23	21, 22	imbi12d 474	. . . . . . . 8 |- (z = A -> ((w (. z -> E.x e. z w ~~ x) <-> (w (. A -> E.x e. A w ~~ x)))
24	23	bialdv 935	. . . . . . 7 |- (z = A -> (A.w(w (. z -> E.x e. z w ~~ x) <-> A.w(w (. A -> E.x e. A w ~~ x)))
25		npss0 1731	. . . . . . . . 9 |- -. w (. (/)
26	25	pm2.21i 73	. . . . . . . 8 |- (w (. (/) -> E.x e. (/) w ~~ x)
27	26	ax-gen 677	. . . . . . 7 |- A.w(w (. (/) -> E.x e. (/) w ~~ x)
28		ax-17 925	. . . . . . . 8 |- (y e. om -> A.w y e. om)
29		hba1 698	. . . . . . . 8 |- (A.w(w (. y -> E.x e. y w ~~ x) -> A.wA.w(w (. y -> E.x e. y w ~~ x))
30		eleq1 1149	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z = y -> (z e. w <-> y e. w))
31	30	biimpcd 137	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (z e. w -> (z = y -> y e. w))
32	31	con3d 87	. . . . . . . . . . . . . . . . . . . . . . 23 |- (z e. w -> (-. y e. w -> -. z = y))
33	32	adantl 305	. . . . . . . . . . . . . . . . . . . . . 22 |- ((w (. suc y /\ z e. w) -> (-. y e. w -> -. z = y))
34		pssss 1567	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w (. suc y -> w (_ suc y)
35	34	sseld 1506	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (w (. suc y -> (z e. w -> z e. suc y))
36		elsuci 2289	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (z e. suc y -> (z e. y \/ z = y))
37	36	ord 202	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z e. suc y -> (-. z e. y -> z = y))
38	37	con1d 85	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (z e. suc y -> (-. z = y -> z e. y))
39	35, 38	syl6 23	. . . . . . . . . . . . . . . . . . . . . . 23 |- (w (. suc y -> (z e. w -> (-. z = y -> z e. y)))
40	39	imp 277	. . . . . . . . . . . . . . . . . . . . . 22 |- ((w (. suc y /\ z e. w) -> (-. z = y -> z e. y))
41	33, 40	syld 27	. . . . . . . . . . . . . . . . . . . . 21 |- ((w (. suc y /\ z e. w) -> (-. y e. w -> z e. y))
42	41	exp 291	. . . . . . . . . . . . . . . . . . . 20 |- (w (. suc y -> (z e. w -> (-. y e. w -> z e. y)))
43	42	com23 32	. . . . . . . . . . . . . . . . . . 19 |- (w (. suc y -> (-. y e. w -> (z e. w -> z e. y)))
44	43	imp 277	. . . . . . . . . . . . . . . . . 18 |- ((w (. suc y /\ -. y e. w) -> (z e. w -> z e. y))
45	44	ssrdv 1509	. . . . . . . . . . . . . . . . 17 |- ((w (. suc y /\ -. y e. w) -> w (_ y)
46	45	anim1i 269	. . . . . . . . . . . . . . . 16 |- (((w (. suc y /\ -. y e. w) /\ -. w = y) -> (w (_ y /\ -. w = y))
47		dfpss2 1557	. . . . . . . . . . . . . . . 16 |- (w (. y <-> (w (_ y /\ -. w = y))
48	46, 47	sylibr 175	. . . . . . . . . . . . . . 15 |- (((w (. suc y /\ -. y e. w) /\ -. w = y) -> w (. y)
49		elelsuc 2295	. . . . . . . . . . . . . . . . 17 |- (x e. y -> x e. suc y)
50	49	anim1i 269	. . . . . . . . . . . . . . . 16 |- ((x e. y /\ w ~~ x) -> (x e. suc y /\ w ~~ x))
51	50	r19.22i2 1274	. . . . . . . . . . . . . . 15 |- (E.x e. y w ~~ x -> E.x e. suc yw ~~ x)
52	48, 51	syl34 20	. . . . . . . . . . . . . 14 |- ((w (. y -> E.x e. y w ~~ x) -> (((w (. suc y /\ -. y e. w) /\ -. w = y) -> E.x e. suc yw ~~ x))
53	52	exp4c 297	. . . . . . . . . . . . 13 |- ((w (. y -> E.x e. y w ~~ x) -> (w (. suc y -> (-. y e. w -> (-. w = y -> E.x e. suc yw ~~ x))))
54	53	a4s 682	. . . . . . . . . . . 12 |- (A.w(w (. y -> E.x e. y w ~~ x) -> (w (. suc y -> (-. y e. w -> (-. w = y -> E.x e. suc yw ~~ x))))
55	54	adantl 305	. . . . . . . . . . 11 |- ((y e. om /\ A.w(w (. y -> E.x e. y w ~~ x)) -> (w (. suc y -> (-. y e. w -> (-. w = y -> E.x e. suc yw ~~ x))))
56	55	com4t 40	. . . . . . . . . 10 |- (-. y e. w -> (-. w = y -> ((y e. om /\ A.w(w (. y -> E.x e. y w ~~ x)) -> (w (. suc y -> E.x e. suc yw ~~ x))))
57		nnord 2381	. . . . . . . . . . . . . . . . . . . . 21 |- (y e. om -> Ord y)
58		orddif 2326	. . . . . . . . . . . . . . . . . . . . 21 |- (Ord y -> y = (suc y \ {y}))
59	57, 58	syl 12	. . . . . . . . . . . . . . . . . . . 20 |- (y e. om -> y = (suc y \ {y}))
60	59	sseq2d 1528	. . . . . . . . . . . . . . . . . . 19 |- (y e. om -> ((w \ {y}) (_ y <-> (w \ {y}) (_ (suc y \ {y})))
61		ssdif 1600	. . . . . . . . . . . . . . . . . . 19 |- (w (_ suc y -> (w \ {y}) (_ (suc y \ {y}))
62	60, 61	syl5bir 184	. . . . . . . . . . . . . . . . . 18 |- (y e. om -> (w (_ suc y -> (w \ {y}) (_ y))
63	62, 34	syl5 22	. . . . . . . . . . . . . . . . 17 |- (y e. om -> (w (. suc y -> (w \ {y}) (_ y))
64		eleq2 1150	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((w \ {y}) = y -> (z e. (w \ {y}) <-> z e. y))
65		eldifi 1591	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (z e. (w \ {y}) -> z e. w)
66	64, 65	syl6bir 188	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((w \ {y}) = y -> (z e. y -> z e. w))
67	66	adantl 305	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((y e. w /\ z e. suc y) /\ (w \ {y}) = y) -> (z e. y -> z e. w))
68		eleq1a 1158	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y e. w -> (z = y -> z e. w))
69	37, 68	sylan9r 360	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((y e. w /\ z e. suc y) -> (-. z e. y -> z e. w))
70	69	adantr 306	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((y e. w /\ z e. suc y) /\ (w \ {y}) = y) -> (-. z e. y -> z e. w))
71	67, 70	pm2.61d 112	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((y e. w /\ z e. suc y) /\ (w \ {y}) = y) -> z e. w)
72	71	exp 291	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y e. w /\ z e. suc y) -> ((w \ {y}) = y -> z e. w))
73	72	con3d 87	. . . . . . . . . . . . . . . . . . . . 21 |- ((y e. w /\ z e. suc y) -> (-. z e. w -> -. (w \ {y}) = y))
74	73	exp 291	. . . . . . . . . . . . . . . . . . . 20 |- (y e. w -> (z e. suc y -> (-. z e. w -> -. (w \ {y}) = y)))
75	74	imp3a 279	. . . . . . . . . . . . . . . . . . 19 |- (y e. w -> ((z e. suc y /\ -. z e. w) -> -. (w \ {y}) = y))
76	75	19.23adv 954	. . . . . . . . . . . . . . . . . 18 |- (y e. w -> (E.z(z e. suc y /\ -. z e. w) -> -. (w \ {y}) = y))
77		pssnel 1752	. . . . . . . . . . . . . . . . . 18 |- (w (. suc y -> E.z(z e. suc y /\ -. z e. w))
78	76, 77	syl5 22	. . . . . . . . . . . . . . . . 17 |- (y