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) Avoid ax-pow . (Revised by BTernaryTau, 31-Jul-2024)

		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	imbitrrid	$⊢ 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	biimtrrdi	$⊢ 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	biimtrrid	$⊢ (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	imbitrrdi	$⊢ (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		disjdifr	$⊢ (w ∖ \{y\}) \cap \{y\} = \emptyset$
108	106 107	jctil	$⊢ x \in ω \to ((w ∖ \{y\}) \cap \{y\} = \emptyset \land x \cap \{x\} = \emptyset)$
109		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\})$
110	103 108 109	syl2an	$⊢ ((w ∖ \{y\}) \approx x \land x \in ω) \to ((w ∖ \{y\}) \cup \{y\}) \approx (x \cup \{x\})$
111		difsnid	$⊢ y \in w \to (w ∖ \{y\}) \cup \{y\} = w$
112	111	eqcomd	$⊢ y \in w \to w = (w ∖ \{y\}) \cup \{y\}$
113		df-suc	$⊢ suc x = x \cup \{x\}$
114	113	a1i	$⊢ y \in w \to suc x = x \cup \{x\}$
115	112 114	breq12d	$⊢ y \in w \to (w \approx suc x \leftrightarrow ((w ∖ \{y\}) \cup \{y\}) \approx (x \cup \{x\}))$
116	110 115	imbitrrid	$⊢ y \in w \to (((w ∖ \{y\}) \approx x \land x \in ω) \to w \approx suc x)$
117	96 116	sylan2i	$⊢ y \in w \to (((w ∖ \{y\}) \approx x \land (x \in y \land y \in ω)) \to w \approx suc x)$
118	117	exp4d	$⊢ y \in w \to ((w ∖ \{y\}) \approx x \to (x \in y \to (y \in ω \to w \approx suc x)))$
119	118	com24	$⊢ y \in w \to (y \in ω \to (x \in y \to ((w ∖ \{y\}) \approx x \to w \approx suc x)))$
120	119	imp4b	$⊢ (y \in w \land y \in ω) \to ((x \in y \land (w ∖ \{y\}) \approx x) \to w \approx suc x)$
121	95 120	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))$
122		breq2	$⊢ z = suc x \to (w \approx z \leftrightarrow w \approx suc x)$
123	122	rspcev	$⊢ (suc x \in suc y \land w \approx suc x) \to \exists z \in suc y w \approx z$
124	121 123	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)$
125	124	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)$
126		df-rex	$⊢ \exists x \in y (w ∖ \{y\}) \approx x \leftrightarrow \exists x (x \in y \land (w ∖ \{y\}) \approx x)$
127		breq2	$⊢ x = z \to (w \approx x \leftrightarrow w \approx z)$
128	127	cbvrexvw	$⊢ \exists x \in suc y w \approx x \leftrightarrow \exists z \in suc y w \approx z$
129	125 126 128	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)$
130	129	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)$
131	90 130	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)$
132	131	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))$
133		eleq1w	$⊢ w = y \to (w \in ω \leftrightarrow y \in ω)$
134	133	pm5.32i	$⊢ (w = y \land w \in ω) \leftrightarrow (w = y \land y \in ω)$
135	82	eqelsuc	$⊢ w = y \to w \in suc y$
136		enrefnn	$⊢ w \in ω \to 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	syl2an	$⊢ (w = y \land w \in ω) \to \exists x \in suc y w \approx x$
140	139	2a1d	$⊢ (w = y \land w \in ω) \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	134 140	sylbir	$⊢ (w = y \land y \in ω) \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))$
142	141	ex	$⊢ w = y \to (y \in ω \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)))$
143	142	adantrd	$⊢ w = y \to ((y \in ω \land \forall w (w \subset y \to \exists x \in y w \approx x)) \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)))$
144	143	pm2.43d	$⊢ 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))$
145	50 132 144	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)$
146	145	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))$
147	24 25 146	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))$
148	8 12 16 20 23 147	finds	$⊢ A \in ω \to \forall w (w \subset A \to \exists x \in A w \approx x)$
149		psseq1	$⊢ w = B \to (w \subset A \leftrightarrow B \subset A)$
150		breq1	$⊢ w = B \to (w \approx x \leftrightarrow B \approx x)$
151	150	rexbidv	$⊢ w = B \to (\exists x \in A w \approx x \leftrightarrow \exists x \in A B \approx x)$
152	149 151	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))$
153	152	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))$
154	148 153	syl5	$⊢ B \in V \to (A \in ω \to (B \subset A \to \exists x \in A B \approx x))$
155	154	com3l	$⊢ A \in ω \to (B \subset A \to (B \in V \to \exists x \in A B \approx x))$
156	155	imp	$⊢ (A \in ω \land B \subset A) \to (B \in V \to \exists x \in A B \approx x)$
157	4 156	mpd	$⊢ (A \in ω \land B \subset A) \to \exists x \in A B \approx x$

Metamath Proof Explorer

Theorem pssnn

Proof