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 ∈ ω ∧ B ⊂ A) → ∃x ∈ A B ≈ x)

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

Proof of Theorem pssnn

Step	Hyp	Ref	Expression
1		ssexg 1702	. . . . . 6 ⊢ (A ∈ ω → (B ⊆ A → B ∈ V))
2		pssss 1567	. . . . . 6 ⊢ (B ⊂ A → B ⊆ A)
3	1, 2	syl5 22	. . . . 5 ⊢ (A ∈ ω → (B ⊂ A → B ∈ 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 → (∃x ∈ A w ≈ x ↔ ∃x ∈ A B ≈ x))
7	4, 6	imbi12d 474	. . . . . . 7 ⊢ (w = B → ((w ⊂ A → ∃x ∈ A w ≈ x) ↔ (B ⊂ A → ∃x ∈ A B ≈ x)))
8	7	cla4gv 1396	. . . . . 6 ⊢ (B ∈ V → (∀w(w ⊂ A → ∃x ∈ A w ≈ x) → (B ⊂ A → ∃x ∈ A B ≈ x)))
9		psseq2 1560	. . . . . . . . 9 ⊢ (z = ∅ → (w ⊂ z ↔ w ⊂ ∅))
10		rexeq 1325	. . . . . . . . 9 ⊢ (z = ∅ → (∃x ∈ z w ≈ x ↔ ∃x ∈ ∅ w ≈ x))
11	9, 10	imbi12d 474	. . . . . . . 8 ⊢ (z = ∅ → ((w ⊂ z → ∃x ∈ z w ≈ x) ↔ (w ⊂ ∅ → ∃x ∈ ∅ w ≈ x)))
12	11	bialdv 935	. . . . . . 7 ⊢ (z = ∅ → (∀w(w ⊂ z → ∃x ∈ z w ≈ x) ↔ ∀w(w ⊂ ∅ → ∃x ∈ ∅ w ≈ x)))
13		psseq2 1560	. . . . . . . . 9 ⊢ (z = y → (w ⊂ z ↔ w ⊂ y))
14		rexeq 1325	. . . . . . . . 9 ⊢ (z = y → (∃x ∈ z w ≈ x ↔ ∃x ∈ y w ≈ x))
15	13, 14	imbi12d 474	. . . . . . . 8 ⊢ (z = y → ((w ⊂ z → ∃x ∈ z w ≈ x) ↔ (w ⊂ y → ∃x ∈ y w ≈ x)))
16	15	bialdv 935	. . . . . . 7 ⊢ (z = y → (∀w(w ⊂ z → ∃x ∈ z w ≈ x) ↔ ∀w(w ⊂ y → ∃x ∈ y w ≈ x)))
17		psseq2 1560	. . . . . . . . 9 ⊢ (z = suc y → (w ⊂ z ↔ w ⊂ suc y))
18		rexeq 1325	. . . . . . . . 9 ⊢ (z = suc y → (∃x ∈ z w ≈ x ↔ ∃x ∈ suc yw ≈ x))
19	17, 18	imbi12d 474	. . . . . . . 8 ⊢ (z = suc y → ((w ⊂ z → ∃x ∈ z w ≈ x) ↔ (w ⊂ suc y → ∃x ∈ suc yw ≈ x)))
20	19	bialdv 935	. . . . . . 7 ⊢ (z = suc y → (∀w(w ⊂ z → ∃x ∈ z w ≈ x) ↔ ∀w(w ⊂ suc y → ∃x ∈ suc yw ≈ x)))
21		psseq2 1560	. . . . . . . . 9 ⊢ (z = A → (w ⊂ z ↔ w ⊂ A))
22		rexeq 1325	. . . . . . . . 9 ⊢ (z = A → (∃x ∈ z w ≈ x ↔ ∃x ∈ A w ≈ x))
23	21, 22	imbi12d 474	. . . . . . . 8 ⊢ (z = A → ((w ⊂ z → ∃x ∈ z w ≈ x) ↔ (w ⊂ A → ∃x ∈ A w ≈ x)))
24	23	bialdv 935	. . . . . . 7 ⊢ (z = A → (∀w(w ⊂ z → ∃x ∈ z w ≈ x) ↔ ∀w(w ⊂ A → ∃x ∈ A w ≈ x)))
25		npss0 1731	. . . . . . . . 9 ⊢ ¬ w ⊂ ∅
26	25	pm2.21i 73	. . . . . . . 8 ⊢ (w ⊂ ∅ → ∃x ∈ ∅ w ≈ x)
27	26	ax-gen 677	. . . . . . 7 ⊢ ∀w(w ⊂ ∅ → ∃x ∈ ∅ w ≈ x)
28		ax-17 925	. . . . . . . 8 ⊢ (y ∈ ω → ∀w y ∈ ω)
29		hba1 698	. . . . . . . 8 ⊢ (∀w(w ⊂ y → ∃x ∈ y w ≈ x) → ∀w∀w(w ⊂ y → ∃x ∈ y w ≈ x))
30		eleq1 1149	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (z = y → (z ∈ w ↔ y ∈ w))
31	30	biimpcd 137	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (z ∈ w → (z = y → y ∈ w))
32	31	con3d 87	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (z ∈ w → (¬ y ∈ w → ¬ z = y))
33	32	adantl 305	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((w ⊂ suc y ∧ z ∈ w) → (¬ y ∈ w → ¬ z = y))
34		pssss 1567	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (w ⊂ suc y → w ⊆ suc y)
35	34	sseld 1506	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (w ⊂ suc y → (z ∈ w → z ∈ suc y))
36		elsuci 2289	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (z ∈ suc y → (z ∈ y ∨ z = y))
37	36	ord 202	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (z ∈ suc y → (¬ z ∈ y → z = y))
38	37	con1d 85	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (z ∈ suc y → (¬ z = y → z ∈ y))
39	35, 38	syl6 23	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (w ⊂ suc y → (z ∈ w → (¬ z = y → z ∈ y)))
40	39	imp 277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((w ⊂ suc y ∧ z ∈ w) → (¬ z = y → z ∈ y))
41	33, 40	syld 27	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((w ⊂ suc y ∧ z ∈ w) → (¬ y ∈ w → z ∈ y))
42	41	exp 291	. . . . . . . . . . . . . . . . . . . 20 ⊢ (w ⊂ suc y → (z ∈ w → (¬ y ∈ w → z ∈ y)))
43	42	com23 32	. . . . . . . . . . . . . . . . . . 19 ⊢ (w ⊂ suc y → (¬ y ∈ w → (z ∈ w → z ∈ y)))
44	43	imp 277	. . . . . . . . . . . . . . . . . 18 ⊢ ((w ⊂ suc y ∧ ¬ y ∈ w) → (z ∈ w → z ∈ y))
45	44	ssrdv 1509	. . . . . . . . . . . . . . . . 17 ⊢ ((w ⊂ suc y ∧ ¬ y ∈ w) → w ⊆ y)
46	45	anim1i 269	. . . . . . . . . . . . . . . 16 ⊢ (((w ⊂ suc y ∧ ¬ y ∈ 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 ∈ w) ∧ ¬ w = y) → w ⊂ y)
49		elelsuc 2295	. . . . . . . . . . . . . . . . 17 ⊢ (x ∈ y → x ∈ suc y)
50	49	anim1i 269	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ y ∧ w ≈ x) → (x ∈ suc y ∧ w ≈ x))
51	50	r19.22i2 1274	. . . . . . . . . . . . . . 15 ⊢ (∃x ∈ y w ≈ x → ∃x ∈ suc yw ≈ x)
52	48, 51	syl34 20	. . . . . . . . . . . . . 14 ⊢ ((w ⊂ y → ∃x ∈ y w ≈ x) → (((w ⊂ suc y ∧ ¬ y ∈ w) ∧ ¬ w = y) → ∃x ∈ suc yw ≈ x))
53	52	exp4c 297	. . . . . . . . . . . . 13 ⊢ ((w ⊂ y → ∃x ∈ y w ≈ x) → (w ⊂ suc y → (¬ y ∈ w → (¬ w = y → ∃x ∈ suc yw ≈ x))))
54	53	a4s 682	. . . . . . . . . . . 12 ⊢ (∀w(w ⊂ y → ∃x ∈ y w ≈ x) → (w ⊂ suc y → (¬ y ∈ w → (¬ w = y → ∃x ∈ suc yw ≈ x))))
55	54	adantl 305	. . . . . . . . . . 11 ⊢ ((y ∈ ω ∧ ∀w(w ⊂ y → ∃x ∈ y w ≈ x)) → (w ⊂ suc y → (¬ y ∈ w → (¬ w = y → ∃x ∈ suc yw ≈ x))))
56	55	com4t 40	. . . . . . . . . 10 ⊢ (¬ y ∈ w → (¬ w = y → ((y ∈ ω ∧ ∀w(w ⊂ y → ∃x ∈ y w ≈ x)) → (w ⊂ suc y → ∃x ∈ suc yw ≈ x))))
57		nnord 2381	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (y ∈ ω → Ord y)
58		orddif 2326	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Ord y → y = (suc y ∖ {y}))
59	57, 58	syl 12	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y ∈ ω → y = (suc y ∖ {y}))
60	59	sseq2d 1528	. . . . . . . . . . . . . . . . . . 19 ⊢ (y ∈ ω → ((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 ∈ ω → (w ⊆ suc y → (w ∖ {y}) ⊆ y))
63	62, 34	syl5 22	. . . . . . . . . . . . . . . . 17 ⊢ (y ∈ ω → (w ⊂ suc y → (w ∖ {y}) ⊆ y))
64		eleq2 1150	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((w ∖ {y}) = y → (z ∈ (w ∖ {y}) ↔ z ∈ y))
65		eldifi 1591	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (z ∈ (w ∖ {y}) → z ∈ w)
66	64, 65	syl6bir 188	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((w ∖ {y}) = y → (z ∈ y → z ∈ w))
67	66	adantl 305	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((y ∈ w ∧ z ∈ suc y) ∧ (w ∖ {y}) = y) → (z ∈ y → z ∈ w))
68		eleq1a 1158	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (y ∈ w → (z = y → z ∈ w))
69	37, 68	sylan9r 360	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((y ∈ w ∧ z ∈ suc y) → (¬ z ∈ y → z ∈ w))
70	69	adantr 306	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((y ∈ w ∧ z ∈ suc y) ∧ (w ∖ {y}) = y) → (¬ z ∈ y → z ∈ w))
71	67, 70	pm2.61d 112	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((y ∈ w ∧ z ∈ suc y) ∧ (w ∖ {y}) = y) → z ∈ w)
72	71	exp 291	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((y ∈ w ∧ z ∈ suc y) → ((w ∖ {y}) = y → z ∈ w))
73	72	con3d 87	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((y ∈ w ∧ z ∈ suc y) → (¬ z ∈ w → ¬ (w ∖ {y}) = y))
74	73	exp 291	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y ∈ w → (z ∈ suc y → (¬ z ∈ w → ¬ (w ∖ {y}) = y)))
75	74	imp3a 279	. . . . . . . . . . . . . . . . . . 19 ⊢ (y ∈ w → ((z ∈ suc y ∧ ¬ z ∈ w) → ¬ (w ∖ {y}) = y))
76	75	19.23adv 954	. . . . . . . . . . . . . . . . . 18 ⊢ (y ∈ w → (∃z(z ∈ suc y ∧ ¬ z ∈ w) → ¬ (w ∖ {y}) = y))
77		pssnel 1752	. . . . . . . . . . . . . . . . . 18 ⊢ (w ⊂ suc y → ∃z(z ∈ suc y ∧ ¬ z ∈ w))
78	76, 77	syl5 22	. . . . . . . . . . . . . . . . 17 ⊢ (y ∈ w → (w ⊂ suc y → ¬ (w ∖ {y}) = y))
79	63, 78	im2anan9r 435	. . . . . . . . . . . . . . . 16 ⊢ ((y ∈ w ∧ y ∈ ω) → ((w ⊂ suc y ∧ w ⊂ suc y) → ((w ∖ {y}) ⊆ y ∧ ¬ (w ∖ {y}) = y)))
80		anidm 331	. . . . . . . . . . . . . . . 16 ⊢ ((w ⊂ suc y ∧ w ⊂ suc y) ↔ w ⊂ suc y)
81	79, 80	syl5ibr 182	. . . . . . . . . . . . . . 15 ⊢ ((y ∈ w ∧ y ∈ ω) → (w ⊂ suc y → ((w ∖ {y}) ⊆ y ∧ ¬ (w ∖ {y}) = y)))
82		dfpss2 1557	. . . . . . . . . . . . . . 15 ⊢ ((w ∖ {y}) ⊂ y ↔ ((w ∖ {y}) ⊆ y ∧ ¬ (w ∖ {y}) = y))
83	81, 82	syl6ibr 186	. . . . . . . . . . . . . 14 ⊢ ((y ∈ w ∧ y ∈ ω) → (w ⊂ suc y → (w ∖ {y}) ⊂ y))
84		psseq1 1559	. . . . . . . . . . . . . . . . 17 ⊢ (w = z → (w ⊂ y ↔ z ⊂ y))
85		breq1 2065	. . . . . . . . . . . . . . . . . 18 ⊢ (w = z → (w ≈ x ↔ z ≈ x))
86	85	birexdv 1220	. . . . . . . . . . . . . . . . 17 ⊢ (w = z → (∃x ∈ y w ≈ x ↔ ∃x ∈ y z ≈ x))
87	84, 86	imbi12d 474	. . . . . . . . . . . . . . . 16 ⊢ (w = z → ((w ⊂ y → ∃x ∈ y w ≈ x) ↔ (z ⊂ y → ∃x ∈ y z ≈ x)))
88	87	cbvalv 972	. . . . . . . . . . . . . . 15 ⊢ (∀w(w ⊂ y → ∃x ∈ y w ≈ x) ↔ ∀z(z ⊂ y → ∃x ∈ y z ≈ x))
89		visset 1350	. . . . . . . . . . . . . . . . 17 ⊢ w ∈ V
90		difss 1596	. . . . . . . . . . . . . . . . 17 ⊢ (w ∖ {y}) ⊆ w
91	89, 90	ssexi 1701	. . . . . . . . . . . . . . . 16 ⊢ (w ∖ {y}) ∈ V
92		psseq1 1559	. . . . . . . . . . . . . . . . 17 ⊢ (z = (w ∖ {y}) → (z ⊂ y ↔ (w ∖ {y}) ⊂ y))
93		breq1 2065	. . . . . . . . . . . . . . . . . 18 ⊢ (z = (w ∖ {y}) → (z ≈ x ↔ (w ∖ {y}) ≈ x))
94	93	birexdv 1220	. . . . . . . . . . . . . . . . 17 ⊢ (z = (w ∖ {y}) → (∃x ∈ y z ≈ x ↔ ∃x ∈ y (w ∖ {y}) ≈ x))
95	92, 94	imbi12d 474	. . . . . . . . . . . . . . . 16 ⊢ (z = (w ∖ {y}) → ((z ⊂ y → ∃x ∈ y z ≈ x) ↔ ((w ∖ {y}) ⊂ y → ∃x ∈ y (w ∖ {y}) ≈ x)))
96	91, 95	cla4v 1400	. . . . . . . . . . . . . . 15 ⊢ (∀z(z ⊂ y → ∃x ∈ y z ≈ x) → ((w ∖ {y}) ⊂ y → ∃x ∈ y (w ∖ {y}) ≈ x))
97	88, 96	sylbi 174	. . . . . . . . . . . . . 14 ⊢ (∀w(w ⊂ y → ∃x ∈ y w ≈ x) → ((w ∖ {y}) ⊂ y → ∃x ∈ y (w ∖ {y}) ≈ x))
98	83, 97	sylan9 359	. . . . . . . . . . . . 13 ⊢ (((y ∈ w ∧ y ∈ ω) ∧ ∀w(w ⊂ y → ∃x ∈ y w ≈ x)) → (w ⊂ suc y → ∃x ∈ y (w ∖ {y}) ≈ x))
99		ordsucelsuc 2324	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Ord y → (x ∈ y ↔ suc x ∈ suc y))
100	99	biimpd 135	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Ord y → (x ∈ y → suc x ∈ suc y))
101	57, 100	syl 12	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y ∈ ω → (x ∈ y → suc x ∈ suc y))
102	101	adantl 305	. . . . . . . . . . . . . . . . . . 19 ⊢ ((y ∈ w ∧ y ∈ ω) → (x ∈ y → suc x ∈ suc y))
103	102	adantrd 308	. . . . . . . . . . . . . . . . . 18 ⊢ ((y ∈ w ∧ y ∈ ω) → ((x ∈ y ∧ (w ∖ {y}) ≈ x) → suc x ∈ suc y))
104		snssi 1851	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (y ∈ w → {y} ⊆ w)
105		ssundif 1764	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({y} ⊆ w ↔ ({y} ∪ (w ∖ {y})) = w)
106	104, 105	sylib 173	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (y ∈ w → ({y} ∪ (w ∖ {y})) = w)
107		uncom 1604	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({y} ∪ (w ∖ {y})) = ((w ∖ {y}) ∪ {y})
108	106, 107	syl5reqr 1139	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (y ∈ w → w = ((w ∖ {y}) ∪ {y}))
109		df-suc 2205	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ suc x = (x ∪ {x})
110	109	a1i 7	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (y ∈ w → suc x = (x ∪ {x}))
111	108, 110	breq12d 2073	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (y ∈ w → (w ≈ suc x ↔ ((w ∖ {y}) ∪ {y}) ≈ (x ∪ {x})))
112		unen 3338	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((w ∖ {y}) ≈ x ∧ {y} ≈ {x}) ∧ (((w ∖ {y}) ∩ {y}) = ∅ ∧ (x ∩ {x}) = ∅)) → ((w ∖ {y}) ∪ {y}) ≈ (x ∪ {x}))
113		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ y ∈ V
114		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ x ∈ V
115	113, 114	f1osn 2827	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ {⟨y, x⟩}:{y}–1-1-onto→{x}
116		snex 1859	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ {y} ∈ V
117	116	f1oen 3301	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({⟨y, x⟩}:{y}–1-1-onto→{x} → {y} ≈ {x})
118	115, 117	ax-mp 6	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {y} ≈ {x}
119	118	jctr 239	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((w ∖ {y}) ≈ x → ((w ∖ {y}) ≈ x ∧ {y} ≈ {x}))
120		nnord 2381	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (x ∈ ω → Ord x)
121		orddisj 2236	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (Ord x → (x ∩ {x}) = ∅)
122	120, 121	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (x ∈ ω → (x ∩ {x}) = ∅)
123		incom 1636	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({y} ∩ (w ∖ {y})) = ((w ∖ {y}) ∩ {y})
124		difdisj 1758	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({y} ∩ (w ∖ {y})) = ∅
125	123, 124	eqtr3 1121	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((w ∖ {y}) ∩ {y}) = ∅
126	122, 125	jctil 240	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (x ∈ ω → (((w ∖ {y}) ∩ {y}) = ∅ ∧ (x ∩ {x}) = ∅))
127	112, 119, 126	syl2an 349	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((w ∖ {y}) ≈ x ∧ x ∈ ω) → ((w ∖ {y}) ∪ {y}) ≈ (x ∪ {x}))
128	111, 127	syl5bir 184	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (y ∈ w → (((w ∖ {y}) ≈ x ∧ x ∈ ω) → w ≈ suc x))
129		elnn 2383	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((x ∈ y ∧ y ∈ ω) → x ∈ ω)
130	128, 129	sylan2i 357	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (y ∈ w → (((w ∖ {y}) ≈ x ∧ (x ∈ y ∧ y ∈ ω)) → w ≈ suc x))
131	130	exp4d 298	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y ∈ w → ((w ∖ {y}) ≈ x → (x ∈ y → (y ∈ ω → w ≈ suc x))))
132	131	com24 37	. . . . . . . . . . . . . . . . . . 19 ⊢ (y ∈ w → (y ∈ ω → (x ∈ y → ((w ∖ {y}) ≈ x → w ≈ suc x))))
133	132	imp4b 283	. . . . . . . . . . . . . . . . . 18 ⊢ ((y ∈ w ∧ y ∈ ω) → ((x ∈ y ∧ (w ∖ {y}) ≈ x) → w ≈ suc x))
134	103, 133	jcad 455	. . . . . . . . . . . . . . . . 17 ⊢ ((y ∈ w ∧ y ∈ ω) → ((x ∈ y ∧ (w ∖ {y}) ≈ x) → (suc x ∈ suc y ∧ w ≈ suc x)))
135		breq2 2066	. . . . . . . . . . . . . . . . . 18 ⊢ (z = suc x → (w ≈ z ↔ w ≈ suc x))
136	135	rcla4ev 1403	. . . . . . . . . . . . . . . . 17 ⊢ ((suc x ∈ suc y ∧ w ≈ suc x) → ∃z ∈ suc yw ≈ z)
137	134, 136	syl6 23	. . . . . . . . . . . . . . . 16 ⊢ ((y ∈ w ∧ y ∈ ω) → ((x ∈ y ∧ (w ∖ {y}) ≈ x) → ∃z ∈ suc yw ≈ z))
138	137	19.23adv 954	. . . . . . . . . . . . . . 15 ⊢ ((y ∈ w ∧ y ∈ ω) → (∃x(x ∈ y ∧ (w ∖ {y}) ≈ x) → ∃z ∈ suc yw ≈ z))
139		df-rex 1206	. . . . . . . . . . . . . . 15 ⊢ (∃x ∈ y (w ∖ {y}) ≈ x ↔ ∃x(x ∈ y ∧ (w ∖ {y}) ≈ x))
140		breq2 2066	. . . . . . . . . . . . . . . 16 ⊢ (x = z → (w ≈ x ↔ w ≈ z))
141	140	cbvrexv 1334	. . . . . . . . . . . . . . 15 ⊢ (∃x ∈ suc yw ≈ x ↔ ∃z ∈ suc yw ≈ z)
142	138, 139, 141	3imtr4g 426	. . . . . . . . . . . . . 14 ⊢ ((y ∈ w ∧ y ∈ ω) → (∃x ∈ y (w ∖ {y}) ≈ x → ∃x ∈ suc yw ≈ x))
143	142	adantr 306	. . . . . . . . . . . . 13 ⊢ (((y ∈ w ∧ y ∈ ω) ∧ ∀w(w ⊂ y → ∃x ∈ y w ≈ x)) → (∃x ∈ y (w ∖ {y}) ≈ x → ∃x ∈ suc yw ≈ x))
144	98, 143	syld 27	. . . . . . . . . . . 12 ⊢ (((y ∈ w ∧ y ∈ ω) ∧ ∀w(w ⊂ y → ∃x ∈ y w ≈ x)) → (w ⊂ suc y → ∃x ∈ suc yw ≈ x))
145	144	exp31 293	. . . . . . . . . . 11 ⊢ (y ∈ w → (y ∈ ω → (∀w(w ⊂ y → ∃x ∈ y w ≈ x) → (w ⊂ suc y → ∃x ∈ suc yw ≈ x))))
146	145	imp3a 279	. . . . . . . . . 10 ⊢ (y ∈ w → ((y ∈ ω ∧ ∀w(w ⊂ y → ∃x ∈ y w ≈ x)) → (w ⊂ suc y → ∃x ∈ suc yw ≈ x)))
147	89	eqelsuc 2307	. . . . . . . . . . . . . 14 ⊢ (w = y → w ∈ suc y)
148	89	enref 3295	. . . . . . . . . . . . . 14 ⊢ w ≈ w
149	147, 148	jctir 241	. . . . . . . . . . . . 13 ⊢ (w = y → (w ∈ suc y ∧ w ≈ w))
150		breq2 2066	. . . . . . . . . . . . . 14 ⊢ (x = w → (w ≈ x ↔ w ≈ w))
151	150	rcla4ev 1403	. . . . . . . . . . . . 13 ⊢ ((w ∈ suc y ∧ w ≈ w) → ∃x ∈ suc yw ≈ x)
152	149, 151	syl 12	. . . . . . . . . . . 12 ⊢ (w = y → ∃x ∈ suc yw ≈ x)
153	152	a1d 14	. . . . . . . . . . 11 ⊢ (w = y → (w ⊂ suc y → ∃x ∈ suc yw ≈ x))
154	153	a1d 14	. . . . . . . . . 10 ⊢ (w = y → ((y ∈ ω ∧ ∀w(w ⊂ y → ∃x ∈ y w ≈ x)) → (w ⊂ suc y → ∃x ∈ suc yw ≈ x)))
155	56, 146, 154	pm2.61ii 113	. . . . . . . . 9 ⊢ ((y ∈ ω ∧ ∀w(w ⊂ y → ∃x ∈ y w ≈ x)) → (w ⊂ suc y → ∃x ∈ suc yw ≈ x))
156	155	exp 291	. . . . . . . 8 ⊢ (y ∈ ω → (∀w(w ⊂ y → ∃x ∈ y w ≈ x) → (w ⊂ suc y → ∃x ∈ suc yw ≈ x)))
157	28, 29, 156	19.21ad 741	. . . . . . 7 ⊢ (y ∈ ω → (∀w(w ⊂ y → ∃x ∈ y w ≈ x) → ∀w(w ⊂ suc y → ∃x ∈ suc yw ≈ x)))
158	12, 16, 20, 24, 27, 157	finds 2397	. . . . . 6 ⊢ (A ∈ ω → ∀w(w ⊂ A → ∃x ∈ A w ≈ x))
159	8, 158	syl5 22	. . . . 5 ⊢ (B ∈ V → (A ∈ ω → (B ⊂ A → ∃x ∈ A B ≈ x)))
160	3, 159	syl6 23	. . . 4 ⊢ (A ∈ ω → (B ⊂ A → (A ∈ ω → (B ⊂ A → ∃x ∈ A B ≈ x))))
161	160	pm2.43a 60	. . 3 ⊢ (A ∈ ω → (B ⊂ A → (B ⊂ A → ∃x ∈ A B ≈ x)))
162	161	pm2.43d 59	. 2 ⊢ (A ∈ ω → (B ⊂ A → ∃x ∈ A B ≈ x))
163	162	imp 277	1 ⊢ ((A ∈ ω ∧ B ⊂ A) → ∃x ∈ A B ≈ x)

Syntax hints:  ¬ wn 1   → wi 2   ∧ wa 196  ∀wal 672  ∃wex 678   = weq 797   ∈ wel 803   = wceq 1091   ∈ wcel 1092  ∃wrex 1202  Vcvv 1348   ∖ cdif 1484   ∪ cun 1485   ∩ cin 1486   ⊆ wss 1487   ⊂ wpss 1488  ∅c0 1707  {csn 1808  ⟨cop 1810   class class class wbr 2054  Ord word 2198  suc csuc 2201  ωcom 2372  –1-1-onto→wf1o 2421   ≈ cen 3271

This theorem is referenced by:  ssnn 3429

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ne 1192  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-pss 1494  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-om 2373  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fo 2436  df-f1o 2437  df-en 3274

metamath.org