Theorem pssnn 4513

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 groups:   x,A   x,B

Proof of Theorem pssnn

Step	Hyp	Ref	Expression
1		ssexg 2711	. . . 4 |- ((B (_ A /\ A e. om) -> B e. V)
2		pssss 2133	. . . 4 |- (B (. A -> B (_ A)
3	1, 2	sylan 448	. . 3 |- ((B (. A /\ A e. om) -> B e. V)
4	3	ancoms 436	. 2 |- ((A e. om /\ B (. A) -> B e. V)
5		psseq1 2125	. . . . . . 7 |- (w = B -> (w (. A <-> B (. A))
6		breq1 2612	. . . . . . . 8 |- (w = B -> (w ~~ x <-> B ~~ x))
7	6	rexbidv 1656	. . . . . . 7 |- (w = B -> (E.x e. A w ~~ x <-> E.x e. A B ~~ x))
8	5, 7	imbi12d 624	. . . . . 6 |- (w = B -> ((w (. A -> E.x e. A w ~~ x) <-> (B (. A -> E.x e. A B ~~ x)))
9	8	cla4gv 1853	. . . . 5 |- (B e. V -> (A.w(w (. A -> E.x e. A w ~~ x) -> (B (. A -> E.x e. A B ~~ x)))
10		psseq2 2126	. . . . . . . 8 |- (z = (/) -> (w (. z <-> w (. (/)))
11		rexeq1 1779	. . . . . . . 8 |- (z = (/) -> (E.x e. z w ~~ x <-> E.x e. (/) w ~~ x))
12	10, 11	imbi12d 624	. . . . . . 7 |- (z = (/) -> ((w (. z -> E.x e. z w ~~ x) <-> (w (. (/) -> E.x e. (/) w ~~ x)))
13	12	albidv 1273	. . . . . 6 |- (z = (/) -> (A.w(w (. z -> E.x e. z w ~~ x) <-> A.w(w (. (/) -> E.x e. (/) w ~~ x)))
14		psseq2 2126	. . . . . . . 8 |- (z = y -> (w (. z <-> w (. y))
15		rexeq1 1779	. . . . . . . 8 |- (z = y -> (E.x e. z w ~~ x <-> E.x e. y w ~~ x))
16	14, 15	imbi12d 624	. . . . . . 7 |- (z = y -> ((w (. z -> E.x e. z w ~~ x) <-> (w (. y -> E.x e. y w ~~ x)))
17	16	albidv 1273	. . . . . 6 |- (z = y -> (A.w(w (. z -> E.x e. z w ~~ x) <-> A.w(w (. y -> E.x e. y w ~~ x)))
18		psseq2 2126	. . . . . . . 8 |- (z = suc y -> (w (. z <-> w (. suc y))
19		rexeq1 1779	. . . . . . . 8 |- (z = suc y -> (E.x e. z w ~~ x <-> E.x e. suc yw ~~ x))
20	18, 19	imbi12d 624	. . . . . . 7 |- (z = suc y -> ((w (. z -> E.x e. z w ~~ x) <-> (w (. suc y -> E.x e. suc yw ~~ x)))
21	20	albidv 1273	. . . . . 6 |- (z = suc y -> (A.w(w (. z -> E.x e. z w ~~ x) <-> A.w(w (. suc y -> E.x e. suc yw ~~ x)))
22		psseq2 2126	. . . . . . . 8 |- (z = A -> (w (. z <-> w (. A))
23		rexeq1 1779	. . . . . . . 8 |- (z = A -> (E.x e. z w ~~ x <-> E.x e. A w ~~ x))
24	22, 23	imbi12d 624	. . . . . . 7 |- (z = A -> ((w (. z -> E.x e. z w ~~ x) <-> (w (. A -> E.x e. A w ~~ x)))
25	24	albidv 1273	. . . . . 6 |- (z = A -> (A.w(w (. z -> E.x e. z w ~~ x) <-> A.w(w (. A -> E.x e. A w ~~ x)))
26		npss0 2299	. . . . . . . 8 |- -. w (. (/)
27	26	pm2.21i 77	. . . . . . 7 |- (w (. (/) -> E.x e. (/) w ~~ x)
28	27	ax-gen 960	. . . . . 6 |- A.w(w (. (/) -> E.x e. (/) w ~~ x)
29		ax-17 968	. . . . . . 7 |- (y e. om -> A.w y e. om)
30		hba1 1000	. . . . . . 7 |- (A.w(w (. y -> E.x e. y w ~~ x) -> A.wA.w(w (. y -> E.x e. y w ~~ x))
31		elequ1 1132	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (z = y -> (z e. w <-> y e. w))
32	31	biimpcd 155	. . . . . . . . . . . . . . . . . . . . . . 23 |- (z e. w -> (z = y -> y e. w))
33	32	con3d 95	. . . . . . . . . . . . . . . . . . . . . 22 |- (z e. w -> (-. y e. w -> -. z = y))
34	33	adantl 388	. . . . . . . . . . . . . . . . . . . . 21 |- ((w (. suc y /\ z e. w) -> (-. y e. w -> -. z = y))
35		pssss 2133	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (w (. suc y -> w (_ suc y)
36	35	sseld 2057	. . . . . . . . . . . . . . . . . . . . . . 23 |- (w (. suc y -> (z e. w -> z e. suc y))
37		elsuci 3025	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z e. suc y -> (z e. y \/ z = y))
38	37	ord 232	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (z e. suc y -> (-. z e. y -> z = y))
39	38	con1d 93	. . . . . . . . . . . . . . . . . . . . . . 23 |- (z e. suc y -> (-. z = y -> z e. y))
40	36, 39	syl6 22	. . . . . . . . . . . . . . . . . . . . . 22 |- (w (. suc y -> (z e. w -> (-. z = y -> z e. y)))
41	40	imp 350	. . . . . . . . . . . . . . . . . . . . 21 |- ((w (. suc y /\ z e. w) -> (-. z = y -> z e. y))
42	34, 41	syld 27	. . . . . . . . . . . . . . . . . . . 20 |- ((w (. suc y /\ z e. w) -> (-. y e. w -> z e. y))
43	42	ex 373	. . . . . . . . . . . . . . . . . . 19 |- (w (. suc y -> (z e. w -> (-. y e. w -> z e. y)))
44	43	com23 32	. . . . . . . . . . . . . . . . . 18 |- (w (. suc y -> (-. y e. w -> (z e. w -> z e. y)))
45	44	imp 350	. . . . . . . . . . . . . . . . 17 |- ((w (. suc y /\ -. y e. w) -> (z e. w -> z e. y))
46	45	ssrdv 2060	. . . . . . . . . . . . . . . 16 |- ((w (. suc y /\ -. y e. w) -> w (_ y)
47	46	anim1i 334	. . . . . . . . . . . . . . 15 |- (((w (. suc y /\ -. y e. w) /\ -. w = y) -> (w (_ y /\ -. w = y))
48		dfpss2 2123	. . . . . . . . . . . . . . 15 |- (w (. y <-> (w (_ y /\ -. w = y))
49	47, 48	sylibr 200	. . . . . . . . . . . . . 14 |- (((w (. suc y /\ -. y e. w) /\ -. w = y) -> w (. y)
50		elelsuc 3031	. . . . . . . . . . . . . . . 16 |- (x e. y -> x e. suc y)
51	50	anim1i 334	. . . . . . . . . . . . . . 15 |- ((x e. y /\ w ~~ x) -> (x e. suc y /\ w ~~ x))
52	51	r19.22i2 1725	. . . . . . . . . . . . . 14 |- (E.x e. y w ~~ x -> E.x e. suc yw ~~ x)
53	49, 52	imim12i 18	. . . . . . . . . . . . 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	exp4c 380	. . . . . . . . . . . 12 |- ((w (. y -> E.x e. y w ~~ x) -> (w (. suc y -> (-. y e. w -> (-. w = y -> E.x e. suc yw ~~ x))))
55	54	a4s 981	. . . . . . . . . . 11 |- (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	adantl 388	. . . . . . . . . 10 |- ((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))))
57	56	com4t 40	. . . . . . . . 9 |- (-. 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))))
58		nnord 3130	. . . . . . . . . . . . . . . . . . . 20 |- (y e. om -> Ord y)
59		orddif 3065	. . . . . . . . . . . . . . . . . . . 20 |- (Ord y -> y = (suc y \ {y}))
60	58, 59	syl 10	. . . . . . . . . . . . . . . . . . 19 |- (y e. om -> y = (suc y \ {y}))
61	60	sseq2d 2079	. . . . . . . . . . . . . . . . . 18 |- (y e. om -> ((w \ {y}) (_ y <-> (w \ {y}) (_ (suc y \ {y})))
62		ssdif 2162	. . . . . . . . . . . . . . . . . 18 |- (w (_ suc y -> (w \ {y}) (_ (suc y \ {y}))
63	61, 62	syl5bir 210	. . . . . . . . . . . . . . . . 17 |- (y e. om -> (w (_ suc y -> (w \ {y}) (_ y))
64	63, 35	syl5 21	. . . . . . . . . . . . . . . 16 |- (y e. om -> (w (. suc y -> (w \ {y}) (_ y))
65		eleq2 1527	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((w \ {y}) = y -> (z e. (w \ {y}) <-> z e. y))
66		eldifi 2152	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z e. (w \ {y}) -> z e. w)
67	65, 66	syl6bir 215	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((w \ {y}) = y -> (z e. y -> z e. w))
68	67	adantl 388	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((y e. w /\ z e. suc y) /\ (w \ {y}) = y) -> (z e. y -> z e. w))
69		eleq1a 1535	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y e. w -> (z = y -> z e. w))
70	38, 69	sylan9r 469	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((y e. w /\ z e. suc y) -> (-. z e. y -> z e. w))
71	70	adantr 389	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((y e. w /\ z e. suc y) /\ (w \ {y}) = y) -> (-. z e. y -> z e. w))
72	68, 71	pm2.61d 127	. . . . . . . . . . . . . . . . . . . . . 22 |- (((y e. w /\ z e. suc y) /\ (w \ {y}) = y) -> z e. w)
73	72	ex 373	. . . . . . . . . . . . . . . . . . . . 21 |- ((y e. w /\ z e. suc y) -> ((w \ {y}) = y -> z e. w))
74	73	con3d 95	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. w /\ z e. suc y) -> (-. z e. w -> -. (w \ {y}) = y))
75	74	ex 373	. . . . . . . . . . . . . . . . . . 19 |- (y e. w -> (z e. suc y -> (-. z e. w -> -. (w \ {y}) = y))