pssnn

Description: A proper subset of a natural number is equinumerous to some smaller number. Lemma 6F of Enderton p. 137. (Contributed by NM, 22-Jun-1998) (Revised by Mario Carneiro, 16-Nov-2014)

		Ref	Expression
	Assertion	pssnn	$⊢ (A \in ω \land B \subset A) \to \exists x \in A B \approx x$

Proof

Step	Hyp	Ref	Expression
1		pssss	$⊢ B \subset A \to B \subseteq A$
2		ssexg	$⊢ (B \subseteq A \land A \in ω) \to B \in V$
3	1 2	sylan	$⊢ (B \subset A \land A \in ω) \to B \in V$
4	3	ancoms	$⊢ (A \in ω \land B \subset A) \to B \in V$
5		psseq2	$⊢ z = \emptyset \to (w \subset z \leftrightarrow w \subset \emptyset)$
6		rexeq	$⊢ z = \emptyset \to (\exists x \in z w \approx x \leftrightarrow \exists x \in \emptyset w \approx x)$
7	5 6	imbi12d	$⊢ z = \emptyset \to ((w \subset z \to \exists x \in z w \approx x) \leftrightarrow (w \subset \emptyset \to \exists x \in \emptyset w \approx x))$
8	7	albidv	$⊢ z = \emptyset \to (\forall w (w \subset z \to \exists x \in z w \approx x) \leftrightarrow \forall w (w \subset \emptyset \to \exists x \in \emptyset w \approx x))$
9		psseq2	$⊢ z = y \to (w \subset z \leftrightarrow w \subset y)$
10		rexeq	$⊢ z = y \to (\exists x \in z w \approx x \leftrightarrow \exists x \in y w \approx x)$
11	9 10	imbi12d	$⊢ z = y \to ((w \subset z \to \exists x \in z w \approx x) \leftrightarrow (w \subset y \to \exists x \in y w \approx x))$
12	11	albidv	$⊢ z = y \to (\forall w (w \subset z \to \exists x \in z w \approx x) \leftrightarrow \forall w (w \subset y \to \exists x \in y w \approx x))$
13		psseq2	$⊢ z = suc y \to (w \subset z \leftrightarrow w \subset suc y)$
14		rexeq	$⊢ z = suc y \to (\exists x \in z w \approx x \leftrightarrow \exists x \in suc y w \approx x)$
15	13 14	imbi12d	$⊢ z = suc y \to ((w \subset z \to \exists x \in z w \approx x) \leftrightarrow (w \subset suc y \to \exists x \in suc y w \approx x))$
16	15	albidv	$⊢ z = suc y \to (\forall w (w \subset z \to \exists x \in z w \approx x) \leftrightarrow \forall w (w \subset suc y \to \exists x \in suc y w \approx x))$
17		psseq2	$⊢ z = A \to (w \subset z \leftrightarrow w \subset A)$
18		rexeq	$⊢ z = A \to (\exists x \in z w \approx x \leftrightarrow \exists x \in A w \approx x)$
19	17 18	imbi12d	$⊢ z = A \to ((w \subset z \to \exists x \in z w \approx x) \leftrightarrow (w \subset A \to \exists x \in A w \approx x))$
20	19	albidv	$⊢ z = A \to (\forall w (w \subset z \to \exists x \in z w \approx x) \leftrightarrow \forall w (w \subset A \to \exists x \in A w \approx x))$
21		npss0	$⊢ \neg w \subset \emptyset$
22	21	pm2.21i	$⊢ w \subset \emptyset \to \exists x \in \emptyset w \approx x$
23	22	ax-gen	$⊢ \forall w (w \subset \emptyset \to \exists x \in \emptyset w \approx x)$
24		nfv	$⊢ Ⅎ w y \in ω$
25		nfa1	$⊢ Ⅎ w \forall w (w \subset y \to \exists x \in y w \approx x)$
26		elequ1	$⊢ z = y \to (z \in w \leftrightarrow y \in w)$
27	26	biimpcd	$⊢ z \in w \to (z = y \to y \in w)$
28	27	con3d	$⊢ z \in w \to (\neg y \in w \to \neg z = y)$
29	28	adantl	$⊢ (w \subset suc y \land z \in w) \to (\neg y \in w \to \neg z = y)$
30		pssss	$⊢ w \subset suc y \to w \subseteq suc y$
31	30	sseld	$⊢ w \subset suc y \to (z \in w \to z \in suc y)$
32		elsuci	$⊢ z \in suc y \to (z \in y \lor z = y)$
33	32	ord	$⊢ z \in suc y \to (\neg z \in y \to z = y)$
34	33	con1d	$⊢ z \in suc y \to (\neg z = y \to z \in y)$
35	31 34	syl6	$⊢ w \subset suc y \to (z \in w \to (\neg z = y \to z \in y))$
36	35	imp	$⊢ (w \subset suc y \land z \in w) \to (\neg z = y \to z \in y)$
37	29 36	syld	$⊢ (w \subset suc y \land z \in w) \to (\neg y \in w \to z \in y)$
38	37	impancom	$⊢ (w \subset suc y \land \neg y \in w) \to (z \in w \to z \in y)$
39	38	ssrdv	$⊢ (w \subset suc y \land \neg y \in w) \to w \subseteq y$
40	39	anim1i	$⊢ ((w \subset suc y \land \neg y \in w) \land \neg w = y) \to (w \subseteq y \land \neg w = y)$
41		dfpss2	$⊢ w \subset y \leftrightarrow (w \subseteq y \land \neg w = y)$
42	40 41	sylibr	$⊢ ((w \subset suc y \land \neg y \in w) \land \neg w = y) \to w \subset y$
43		elelsuc	$⊢ x \in y \to x \in suc y$
44	43	anim1i	$⊢ (x \in y \land w \approx x) \to (x \in suc y \land w \approx x)$
45	44	reximi2	$⊢ \exists x \in y w \approx x \to \exists x \in suc y w \approx x$
46	42 45	imim12i	$⊢ (w \subset y \to \exists x \in y w \approx x) \to (((w \subset suc y \land \neg y \in w) \land \neg w = y) \to \exists x \in suc y w \approx x)$
47	46	exp4c	$⊢ (w \subset y \to \exists x \in y w \approx x) \to (w \subset suc y \to (\neg y \in w \to (\neg w = y \to \exists x \in suc y w \approx x)))$
48	47	sps	$⊢ \forall w (w \subset y \to \exists x \in y w \approx x) \to (w \subset suc y \to (\neg y \in w \to (\neg w = y \to \exists x \in suc y w \approx x)))$
49	48	adantl	$⊢ (y \in ω \land \forall w (w \subset y \to \exists x \in y w \approx x)) \to (w \subset suc y \to (\neg y \in w \to (\neg w = y \to \exists x \in suc y w \approx x)))$
50	49	com4t	$⊢ \neg y \in w \to (\neg w = y \to ((y \in ω \land \forall w (w \subset y \to \exists x \in y w \approx x)) \to (w \subset suc y \to \exists x \in suc y w \approx x)))$
51		anidm	$⊢ (w \subset suc y \land w \subset suc y) \leftrightarrow w \subset suc y$
52		ssdif	$⊢ w \subseteq suc y \to w ∖ \{y\} \subseteq suc y ∖ \{y\}$
53		nnord	$⊢ y \in ω \to Ord y$
54		orddif	$⊢ Ord y \to y = suc y ∖ \{y\}$
55	53 54	syl	$⊢ y \in ω \to y = suc y ∖ \{y\}$
56	55	sseq2d	$⊢ y \in ω \to (w ∖ \{y\} \subseteq y \leftrightarrow w ∖ \{y\} \subseteq suc y ∖ \{y\})$
57	52 56	syl5ibr	$⊢ y \in ω \to (w \subseteq suc y \to w ∖ \{y\} \subseteq y)$
58	30 57	syl5	$⊢ y \in ω \to (w \subset suc y \to w ∖ \{y\} \subseteq y)$
59		pssnel	$⊢ w \subset suc y \to \exists z (z \in suc y \land \neg z \in w)$
60		eleq2	$⊢ w ∖ \{y\} = y \to (z \in (w ∖ \{y\}) \leftrightarrow z \in y)$
61		eldifi	$⊢ z \in (w ∖ \{y\}) \to z \in w$
62	60 61	syl6bir	$⊢ w ∖ \{y\} = y \to (z \in y \to z \in w)$
63	62	adantl	$⊢ ((y \in w \land z \in suc y) \land w ∖ \{y\} = y) \to (z \in y \to z \in w)$
64		eleq1a	$⊢ y \in w \to (z = y \to z \in w)$
65	33 64	sylan9r	$⊢ (y \in w \land z \in suc y) \to (\neg z \in y \to z \in w)$
66	65	adantr	$⊢ ((y \in w \land z \in suc y) \land w ∖ \{y\} = y) \to (\neg z \in y \to z \in w)$
67	63 66	pm2.61d	$⊢ ((y \in w \land z \in suc y) \land w ∖ \{y\} = y) \to z \in w$
68	67	ex	$⊢ (y \in w \land z \in suc y) \to (w ∖ \{y\} = y \to z \in w)$
69	68	con3d	$⊢ (y \in w \land z \in suc y) \to (\neg z \in w \to \neg w ∖ \{y\} = y)$
70	69	expimpd	$⊢ y \in w \to ((z \in suc y \land \neg z \in w) \to \neg w ∖ \{y\} = y)$
71	70	exlimdv	$⊢ y \in w \to (\exists z (z \in suc y \land \neg z \in w) \to \neg w ∖ \{y\} = y)$
72	59 71	syl5	$⊢ y \in w \to (w \subset suc y \to \neg w ∖ \{y\} = y)$
73	58 72	im2anan9r	$⊢ (y \in w \land y \in ω) \to ((w \subset suc y \land w \subset suc y) \to (w ∖ \{y\} \subseteq y \land \neg w ∖ \{y\} = y))$
74	51 73	syl5bir	$⊢ (y \in w \land y \in ω) \to (w \subset suc y \to (w ∖ \{y\} \subseteq y \land \neg w ∖ \{y\} = y))$
75		dfpss2	$⊢ w ∖ \{y\} \subset y \leftrightarrow (w ∖ \{y\} \subseteq y \land \neg w ∖ \{y\} = y)$
76	74 75	syl6ibr	$⊢ (y \in w \land y \in ω) \to (w \subset suc y \to w ∖ \{y\} \subset y)$
77		psseq1	$⊢ w = z \to (w \subset y \leftrightarrow z \subset y)$
78		breq1	$⊢ w = z \to (w \approx x \leftrightarrow z \approx x)$
79	78	rexbidv	$⊢ w = z \to (\exists x \in y w \approx x \leftrightarrow \exists x \in y z \approx x)$
80	77 79	imbi12d	$⊢ w = z \to ((w \subset y \to \exists x \in y w \approx x) \leftrightarrow (z \subset y \to \exists x \in y z \approx x))$
81	80	cbvalvw	$⊢ \forall w (w \subset y \to \exists x \in y w \approx x) \leftrightarrow \forall z (z \subset y \to \exists x \in y z \approx x)$
82		vex	$⊢ w \in V$
83	82	difexi	$⊢ w ∖ \{y\} \in V$
84		psseq1	$⊢ z = w ∖ \{y\} \to (z \subset y \leftrightarrow w ∖ \{y\} \subset y)$
85		breq1	$⊢ z = w ∖ \{y\} \to (z \approx x \leftrightarrow (w ∖ \{y\}) \approx x)$
86	85	rexbidv	$⊢ z = w ∖ \{y\} \to (\exists x \in y z \approx x \leftrightarrow \exists x \in y (w ∖ \{y\}) \approx x)$
87	84 86	imbi12d	$⊢ z = w ∖ \{y\} \to ((z \subset y \to \exists x \in y z \approx x) \leftrightarrow (w ∖ \{y\} \subset y \to \exists x \in y (w ∖ \{y\}) \approx x))$
88	83 87	spcv	$⊢ \forall z (z \subset y \to \exists x \in y z \approx x) \to (w ∖ \{y\} \subset y \to \exists x \in y (w ∖ \{y\}) \approx x)$
89	81 88	sylbi	$⊢ \forall w (w \subset y \to \exists x \in y w \approx x) \to (w ∖ \{y\} \subset y \to \exists x \in y (w ∖ \{y\}) \approx x)$
90	76 89	sylan9	$⊢ ((y \in w \land y \in ω) \land \forall w (w \subset y \to \exists x \in y w \approx x)) \to (w \subset suc y \to \exists x \in y (w ∖ \{y\}) \approx x)$
91		ordsucelsuc	$⊢ Ord y \to (x \in y \leftrightarrow suc x \in suc y)$
92	91	biimpd	$⊢ Ord y \to (x \in y \to suc x \in suc y)$
93	53 92	syl	$⊢ y \in ω \to (x \in y \to suc x \in suc y)$
94	93	adantl	$⊢ (y \in w \land y \in ω) \to (x \in y \to suc x \in suc y)$
95	94	adantrd	$⊢ (y \in w \land y \in ω) \to ((x \in y \land (w ∖ \{y\}) \approx x) \to suc x \in suc y)$
96		elnn	$⊢ (x \in y \land y \in ω) \to x \in ω$
97		snex	$⊢ \{⟨y, x⟩\} \in V$
98		vex	$⊢ y \in V$
99		vex	$⊢ x \in V$
100	98 99	f1osn	$⊢ \{⟨y, x⟩\} : \{y\} \underset{1-1 onto}{⟶} \{x\}$
101		f1oen3g	$⊢ (\{⟨y, x⟩\} \in V \land \{⟨y, x⟩\} : \{y\} \underset{1-1 onto}{⟶} \{x\}) \to \{y\} \approx \{x\}$
102	97 100 101	mp2an	$⊢ \{y\} \approx \{x\}$
103	102	jctr	$⊢ (w ∖ \{y\}) \approx x \to ((w ∖ \{y\}) \approx x \land \{y\} \approx \{x\})$
104		nnord	$⊢ x \in ω \to Ord x$
105		orddisj	$⊢ Ord x \to x \cap \{x\} = \emptyset$
106	104 105	syl	$⊢ x \in ω \to x \cap \{x\} = \emptyset$
107		incom	$⊢ \{y\} \cap (w ∖ \{y\}) = (w ∖ \{y\}) \cap \{y\}$
108		disjdif	$⊢ \{y\} \cap (w ∖ \{y\}) = \emptyset$
109	107 108	eqtr3i	$⊢ (w ∖ \{y\}) \cap \{y\} = \emptyset$
110	106 109	jctil	$⊢ x \in ω \to ((w ∖ \{y\}) \cap \{y\} = \emptyset \land x \cap \{x\} = \emptyset)$
111		unen	$⊢ (((w ∖ \{y\}) \approx x \land \{y\} \approx \{x\}) \land ((w ∖ \{y\}) \cap \{y\} = \emptyset \land x \cap \{x\} = \emptyset)) \to ((w ∖ \{y\}) \cup \{y\}) \approx (x \cup \{x\})$
112	103 110 111	syl2an	$⊢ ((w ∖ \{y\}) \approx x \land x \in ω) \to ((w ∖ \{y\}) \cup \{y\}) \approx (x \cup \{x\})$
113		difsnid	$⊢ y \in w \to (w ∖ \{y\}) \cup \{y\} = w$
114	113	eqcomd	$⊢ y \in w \to w = (w ∖ \{y\}) \cup \{y\}$
115		df-suc	$⊢ suc x = x \cup \{x\}$
116	115	a1i	$⊢ y \in w \to suc x = x \cup \{x\}$
117	114 116	breq12d	$⊢ y \in w \to (w \approx suc x \leftrightarrow ((w ∖ \{y\}) \cup \{y\}) \approx (x \cup \{x\}))$
118	112 117	syl5ibr	$⊢ y \in w \to (((w ∖ \{y\}) \approx x \land x \in ω) \to w \approx suc x)$
119	96 118	sylan2i	$⊢ y \in w \to (((w ∖ \{y\}) \approx x \land (x \in y \land y \in ω)) \to w \approx suc x)$
120	119	exp4d	$⊢ y \in w \to ((w ∖ \{y\}) \approx x \to (x \in y \to (y \in ω \to w \approx suc x)))$
121	120	com24	$⊢ y \in w \to (y \in ω \to (x \in y \to ((w ∖ \{y\}) \approx x \to w \approx suc x)))$
122	121	imp4b	$⊢ (y \in w \land y \in ω) \to ((x \in y \land (w ∖ \{y\}) \approx x) \to w \approx suc x)$
123	95 122	jcad	$⊢ (y \in w \land y \in ω) \to ((x \in y \land (w ∖ \{y\}) \approx x) \to (suc x \in suc y \land w \approx suc x))$
124		breq2	$⊢ z = suc x \to (w \approx z \leftrightarrow w \approx suc x)$
125	124	rspcev	$⊢ (suc x \in suc y \land w \approx suc x) \to \exists z \in suc y w \approx z$
126	123 125	syl6	$⊢ (y \in w \land y \in ω) \to ((x \in y \land (w ∖ \{y\}) \approx x) \to \exists z \in suc y w \approx z)$
127	126	exlimdv	$⊢ (y \in w \land y \in ω) \to (\exists x (x \in y \land (w ∖ \{y\}) \approx x) \to \exists z \in suc y w \approx z)$
128		df-rex	$⊢ \exists x \in y (w ∖ \{y\}) \approx x \leftrightarrow \exists x (x \in y \land (w ∖ \{y\}) \approx x)$
129		breq2	$⊢ x = z \to (w \approx x \leftrightarrow w \approx z)$
130	129	cbvrexvw	$⊢ \exists x \in suc y w \approx x \leftrightarrow \exists z \in suc y w \approx z$
131	127 128 130	3imtr4g	$⊢ (y \in w \land y \in ω) \to (\exists x \in y (w ∖ \{y\}) \approx x \to \exists x \in suc y w \approx x)$
132	131	adantr	$⊢ ((y \in w \land y \in ω) \land \forall w (w \subset y \to \exists x \in y w \approx x)) \to (\exists x \in y (w ∖ \{y\}) \approx x \to \exists x \in suc y w \approx x)$
133	90 132	syld	$⊢ ((y \in w \land y \in ω) \land \forall w (w \subset y \to \exists x \in y w \approx x)) \to (w \subset suc y \to \exists x \in suc y w \approx x)$
134	133	expl	$⊢ y \in w \to ((y \in ω \land \forall w (w \subset y \to \exists x \in y w \approx x)) \to (w \subset suc y \to \exists x \in suc y w \approx x))$
135	82	eqelsuc	$⊢ w = y \to w \in suc y$
136	82	enref	$⊢ w \approx w$
137		breq2	$⊢ x = w \to (w \approx x \leftrightarrow w \approx w)$
138	137	rspcev	$⊢ (w \in suc y \land w \approx w) \to \exists x \in suc y w \approx x$
139	135 136 138	sylancl	$⊢ w = y \to \exists x \in suc y w \approx x$
140	139	2a1d	$⊢ w = y \to ((y \in ω \land \forall w (w \subset y \to \exists x \in y w \approx x)) \to (w \subset suc y \to \exists x \in suc y w \approx x))$
141	50 134 140	pm2.61ii	$⊢ (y \in ω \land \forall w (w \subset y \to \exists x \in y w \approx x)) \to (w \subset suc y \to \exists x \in suc y w \approx x)$
142	141	ex	$⊢ y \in ω \to (\forall w (w \subset y \to \exists x \in y w \approx x) \to (w \subset suc y \to \exists x \in suc y w \approx x))$
143	24 25 142	alrimd	$⊢ y \in ω \to (\forall w (w \subset y \to \exists x \in y w \approx x) \to \forall w (w \subset suc y \to \exists x \in suc y w \approx x))$
144	8 12 16 20 23 143	finds	$⊢ A \in ω \to \forall w (w \subset A \to \exists x \in A w \approx x)$
145		psseq1	$⊢ w = B \to (w \subset A \leftrightarrow B \subset A)$
146		breq1	$⊢ w = B \to (w \approx x \leftrightarrow B \approx x)$
147	146	rexbidv	$⊢ w = B \to (\exists x \in A w \approx x \leftrightarrow \exists x \in A B \approx x)$
148	145 147	imbi12d	$⊢ w = B \to ((w \subset A \to \exists x \in A w \approx x) \leftrightarrow (B \subset A \to \exists x \in A B \approx x))$
149	148	spcgv	$⊢ B \in V \to (\forall w (w \subset A \to \exists x \in A w \approx x) \to (B \subset A \to \exists x \in A B \approx x))$
150	144 149	syl5	$⊢ B \in V \to (A \in ω \to (B \subset A \to \exists x \in A B \approx x))$
151	150	com3l	$⊢ A \in ω \to (B \subset A \to (B \in V \to \exists x \in A B \approx x))$
152	151	imp	$⊢ (A \in ω \land B \subset A) \to (B \in V \to \exists x \in A B \approx x)$
153	4 152	mpd	$⊢ (A \in ω \land B \subset A) \to \exists x \in A B \approx x$

Metamath Proof Explorer

Theorem pssnn

Proof