Theorem pssnn 4522

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

Proof of Theorem pssnn

Step	Hyp	Ref	Expression
1		ssexg 2717	. . . 4 ⊢ ((B ⊆ A ⋀ A ∈ ω) → B ∈ V)
2		pssss 2140	. . . 4 ⊢ (B ⊂ A → B ⊆ A)
3	1, 2	sylan 448	. . 3 ⊢ ((B ⊂ A ⋀ A ∈ ω) → B ∈ V)
4	3	ancoms 436	. 2 ⊢ ((A ∈ ω ⋀ B ⊂ A) → B ∈ V)
5		psseq1 2132	. . . . . . 7 ⊢ (w = B → (w ⊂ A ↔ B ⊂ A))
6		breq1 2618	. . . . . . . 8 ⊢ (w = B → (w ≈ x ↔ B ≈ x))
7	6	rexbidv 1662	. . . . . . 7 ⊢ (w = B → (∃x ∈ A w ≈ x ↔ ∃x ∈ A B ≈ x))
8	5, 7	imbi12d 625	. . . . . 6 ⊢ (w = B → ((w ⊂ A → ∃x ∈ A w ≈ x) ↔ (B ⊂ A → ∃x ∈ A B ≈ x)))
9	8	cla4gv 1859	. . . . 5 ⊢ (B ∈ V → (∀w(w ⊂ A → ∃x ∈ A w ≈ x) → (B ⊂ A → ∃x ∈ A B ≈ x)))
10		psseq2 2133	. . . . . . . 8 ⊢ (z = ∅ → (w ⊂ z ↔ w ⊂ ∅))
11		rexeq1 1785	. . . . . . . 8 ⊢ (z = ∅ → (∃x ∈ z w ≈ x ↔ ∃x ∈ ∅ w ≈ x))
12	10, 11	imbi12d 625	. . . . . . 7 ⊢ (z = ∅ → ((w ⊂ z → ∃x ∈ z w ≈ x) ↔ (w ⊂ ∅ → ∃x ∈ ∅ w ≈ x)))
13	12	albidv 1277	. . . . . 6 ⊢ (z = ∅ → (∀w(w ⊂ z → ∃x ∈ z w ≈ x) ↔ ∀w(w ⊂ ∅ → ∃x ∈ ∅ w ≈ x)))
14		psseq2 2133	. . . . . . . 8 ⊢ (z = y → (w ⊂ z ↔ w ⊂ y))
15		rexeq1 1785	. . . . . . . 8 ⊢ (z = y → (∃x ∈ z w ≈ x ↔ ∃x ∈ y w ≈ x))
16	14, 15	imbi12d 625	. . . . . . 7 ⊢ (z = y → ((w ⊂ z → ∃x ∈ z w ≈ x) ↔ (w ⊂ y → ∃x ∈ y w ≈ x)))
17	16	albidv 1277	. . . . . 6 ⊢ (z = y → (∀w(w ⊂ z → ∃x ∈ z w ≈ x) ↔ ∀w(w ⊂ y → ∃x ∈ y w ≈ x)))
18		psseq2 2133	. . . . . . . 8 ⊢ (z = suc y → (w ⊂ z ↔ w ⊂ suc y))
19		rexeq1 1785	. . . . . . . 8 ⊢ (z = suc y → (∃x ∈ z w ≈ x ↔ ∃x ∈ suc yw ≈ x))
20	18, 19	imbi12d 625	. . . . . . 7 ⊢ (z = suc y → ((w ⊂ z → ∃x ∈ z w ≈ x) ↔ (w ⊂ suc y → ∃x ∈ suc yw ≈ x)))
21	20	albidv 1277	. . . . . 6 ⊢ (z = suc y → (∀w(w ⊂ z → ∃x ∈ z w ≈ x) ↔ ∀w(w ⊂ suc y → ∃x ∈ suc yw ≈ x)))
22		psseq2 2133	. . . . . . . 8 ⊢ (z = A → (w ⊂ z ↔ w ⊂ A))
23		rexeq1 1785	. . . . . . . 8 ⊢ (z = A → (∃x ∈ z w ≈ x ↔ ∃x ∈ A w ≈ x))
24	22, 23	imbi12d 625	. . . . . . 7 ⊢ (z = A → ((w ⊂ z → ∃x ∈ z w ≈ x) ↔ (w ⊂ A → ∃x ∈ A w ≈ x)))
25	24	albidv 1277	. . . . . 6 ⊢ (z = A → (∀w(w ⊂ z → ∃x ∈ z w ≈ x) ↔ ∀w(w ⊂ A → ∃x ∈ A w ≈ x)))
26		npss0 2306	. . . . . . . 8 ⊢ ¬ w ⊂ ∅
27	26	pm2.21i 77	. . . . . . 7 ⊢ (w ⊂ ∅ → ∃x ∈ ∅ w ≈ x)
28	27	ax-gen 962	. . . . . 6 ⊢ ∀w(w ⊂ ∅ → ∃x ∈ ∅ w ≈ x)
29		ax-17 970	. . . . . . 7 ⊢ (y ∈ ω → ∀w y ∈ ω)
30		hba1 1002	. . . . . . 7 ⊢ (∀w(w ⊂ y → ∃x ∈ y w ≈ x) → ∀w∀w(w ⊂ y → ∃x ∈ y w ≈ x))
31		elequ1 1135	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (z = y → (z ∈ w ↔ y ∈ w))
32	31	biimpcd 155	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (z ∈ w → (z = y → y ∈ w))
33	32	con3d 95	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (z ∈ w → (¬ y ∈ w → ¬ z = y))
34	33	adantl 388	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((w ⊂ suc y ⋀ z ∈ w) → (¬ y ∈ w → ¬ z = y))
35		pssss 2140	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (w ⊂ suc y → w ⊆ suc y)
36	35	sseld 2064	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (w ⊂ suc y → (z ∈ w → z ∈ suc y))
37		elsuci 3031	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (z ∈ suc y → (z ∈ y ⋁ z = y))
38	37	ord 232	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (z ∈ suc y → (¬ z ∈ y → z = y))
39	38	con1d 93	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (z ∈ suc y → (¬ z = y → z ∈ y))
40	36, 39	syl6 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (w ⊂ suc y → (z ∈ w → (¬ z = y → z ∈ y)))
41	40	imp 350	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((w ⊂ suc y ⋀ z ∈ w) → (¬ z = y → z ∈ y))
42	34, 41	syld 27	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((w ⊂ suc y ⋀ z ∈ w) → (¬ y ∈ w → z ∈ y))
43	42	ex 373	. . . . . . . . . . . . . . . . . . 19 ⊢ (w ⊂ suc y → (z ∈ w → (¬ y ∈ w → z ∈ y)))
44	43	com23 32	. . . . . . . . . . . . . . . . . 18 ⊢ (w ⊂ suc y → (¬ y ∈ w → (z ∈ w → z ∈ y)))
45	44	imp 350	. . . . . . . . . . . . . . . . 17 ⊢ ((w ⊂ suc y ⋀ ¬ y ∈ w) → (z ∈ w → z ∈ y))
46	45	ssrdv 2067	. . . . . . . . . . . . . . . 16 ⊢ ((w ⊂ suc y ⋀ ¬ y ∈ w) → w ⊆ y)
47	46	anim1i 334	. . . . . . . . . . . . . . 15 ⊢ (((w ⊂ suc y ⋀ ¬ y ∈ w) ⋀ ¬ w = y) → (w ⊆ y ⋀ ¬ w = y))
48		dfpss2 2130	. . . . . . . . . . . . . . 15 ⊢ (w ⊂ y ↔ (w ⊆ y ⋀ ¬ w = y))
49	47, 48	sylibr 200	. . . . . . . . . . . . . 14 ⊢ (((w ⊂ suc y ⋀ ¬ y ∈ w) ⋀ ¬ w = y) → w ⊂ y)
50		elelsuc 3037	. . . . . . . . . . . . . . . 16 ⊢ (x ∈ y → x ∈ suc y)
51	50	anim1i 334	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ y ⋀ w ≈ x) → (x ∈ suc y ⋀ w ≈ x))
52	51	r19.22i2 1731	. . . . . . . . . . . . . 14 ⊢ (∃x ∈ y w ≈ x → ∃x ∈ suc yw ≈ x)
53	49, 52	imim12i 18	. . . . . . . . . . . . 13 ⊢ ((w ⊂ y → ∃x ∈ y w ≈ x) → (((w ⊂ suc y ⋀ ¬ y ∈ w) ⋀ ¬ w = y) → ∃x ∈ suc yw ≈ x))
54	53	exp4c 380	. . . . . . . . . . . 12 ⊢ ((w ⊂ y → ∃x ∈ y w ≈ x) → (w ⊂ suc y → (¬ y ∈ w → (¬ w = y → ∃x ∈ suc yw ≈ x))))
55	54	a4s 983	. . . . . . . . . . 11 ⊢ (∀w(w ⊂ y → ∃x ∈ y w ≈ x) → (w ⊂ suc y → (¬ y ∈ w → (¬ w = y → ∃x ∈ suc yw ≈ x))))
56	55	adantl 388	. . . . . . . . . 10 ⊢ ((y ∈ ω ⋀ ∀w(w ⊂ y → ∃x ∈ y w ≈ x)) → (w ⊂ suc y → (¬ y ∈ w → (¬ w = y → ∃x ∈ suc yw ≈ x))))
57	56	com4t 40	. . . . . . . . 9 ⊢ (¬ y ∈ w → (¬ w = y → ((y ∈ ω ⋀ ∀w(w ⊂ y → ∃x ∈ y w ≈ x)) → (w ⊂ suc y → ∃x ∈ suc yw ≈ x))))
58		nnord 3136	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y ∈ ω → Ord y)
59		orddif 3071	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Ord y → y = (suc y ∖ {y}))
60	58, 59	syl 10	. . . . . . . . . . . . . . . . . . 19 ⊢ (y ∈ ω → y = (suc y ∖ {y}))
61	60	sseq2d 2086	. . . . . . . . . . . . . . . . . 18 ⊢ (y ∈ ω → ((w ∖ {y}) ⊆ y ↔ (w ∖ {y}) ⊆ (suc y ∖ {y})))
62		ssdif 2169	. . . . . . . . . . . . . . . . . 18 ⊢ (w ⊆ suc y → (w ∖ {y}) ⊆ (suc y ∖ {y}))
63	61, 62	syl5bir 210	. . . . . . . . . . . . . . . . 17 ⊢ (y ∈ ω → (w ⊆ suc y → (w ∖ {y}) ⊆ y))
64	63, 35	syl5 21	. . . . . . . . . . . . . . . 16 ⊢ (y ∈ ω → (w ⊂ suc y → (w ∖ {y}) ⊆ y))
65		eleq2 1533	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((w ∖ {y}) = y → (z ∈ (w ∖ {y}) ↔ z ∈ y))
66		eldifi 2159	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (z ∈ (w ∖ {y}) → z ∈ w)
67	65, 66	syl6bir 215	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((w ∖ {y}) = y → (z ∈ y → z ∈ w))
68	67	adantl 388	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((y ∈ w ⋀ z ∈ suc y) ⋀ (w ∖ {y}) = y) → (z ∈ y → z ∈ w))
69		eleq1a 1541	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (y ∈ w → (z = y → z ∈ w))
70	38, 69	sylan9r 469	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((y ∈ w ⋀ z ∈ suc y) → (¬ z ∈ y → z ∈ w))
71	70	adantr 389	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((y ∈ w ⋀ z ∈ suc y) ⋀ (w ∖ {y}) = y) → (¬ z ∈ y → z ∈ w))
72	68, 71	pm2.61d 127	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((y ∈ w ⋀ z ∈ suc y) ⋀ (w ∖ {y}) = y) → z ∈ w)
73	72	ex 373	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((y ∈ w ⋀ z ∈ suc y) → ((w ∖ {y}) = y → z ∈ w))
74	73	con3d 95	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y ∈ w ⋀ z ∈ suc y) → (¬ z ∈ w → ¬ (w ∖ {y}) = y))
75	74	ex 373	. . . . . . . . . . . . . . . . . . 19 ⊢ (y ∈ w → (z ∈ suc y → (¬ z ∈ w → ¬ (w ∖ {y}) = y)))
76	75	imp3a 361	. . . . . . . . . . . . . . . . . 18 ⊢ (y ∈ w → ((z ∈ suc y ⋀ ¬ z ∈ w) → ¬ (w ∖ {y}) = y))
77	76	19.23adv 1213	. . . . . . . . . . . . . . . . 17 ⊢ (y ∈ w → (∃z(z ∈ suc y ⋀ ¬ z ∈ w) → ¬ (w ∖ {y}) = y))
78		pssnel 2328	. . . . . . . . . . . . . . . . 17 ⊢ (w ⊂ suc y → ∃z(z ∈ suc y ⋀ ¬ z ∈ w))
79	77, 78	syl5 21	. . . . . . . . . . . . . . . 16 ⊢ (y ∈ w → (w ⊂ suc y → ¬ (w ∖ {y}) = y))
80	64, 79	im2anan9r 563	. . . . . . . . . . . . . . 15 ⊢ ((y ∈ w ⋀ y ∈ ω) → ((w ⊂ suc y ⋀ w ⊂ suc y) → ((w ∖ {y}) ⊆ y ⋀ ¬ (w ∖ {y}) = y)))
81		anidm 432	. . . . . . . . . . . . . . 15 ⊢ ((w ⊂ suc y ⋀ w ⊂ suc y) ↔ w ⊂ suc y)
82	80, 81	syl5ibr 207	. . . . . . . . . . . . . 14 ⊢ ((y ∈ w ⋀ y ∈ ω) → (w ⊂ suc y → ((w ∖ {y}) ⊆ y ⋀ ¬ (w ∖ {y}) = y)))
83		dfpss2 2130	. . . . . . . . . . . . . 14 ⊢ ((w ∖ {y}) ⊂ y ↔ ((w ∖ {y}) ⊆ y ⋀ ¬ (w ∖ {y}) = y))
84	82, 83	syl6ibr 213	. . . . . . . . . . . . 13 ⊢ ((y ∈ w ⋀ y ∈ ω) → (w ⊂ suc y → (w ∖ {y}) ⊂ y))
85		psseq1 2132	. . . . . . . . . . . . . . . 16 ⊢ (w = z → (w ⊂ y ↔ z ⊂ y))
86		breq1 2618	. . . . . . . . . . . . . . . . 17 ⊢ (w = z → (w ≈ x ↔ z ≈ x))
87	86	rexbidv 1662	. . . . . . . . . . . . . . . 16 ⊢ (w = z → (∃x ∈ y w ≈ x ↔ ∃x ∈ y z ≈ x))
88	85, 87	imbi12d 625	. . . . . . . . . . . . . . 15 ⊢ (w = z → ((w ⊂ y → ∃x ∈ y w ≈ x) ↔ (z ⊂ y → ∃x ∈ y z ≈ x)))
89	88	cbvalv 1313	. . . . . . . . . . . . . 14 ⊢ (∀w(w ⊂ y → ∃x ∈ y w ≈ x) ↔ ∀z(z ⊂ y → ∃x ∈ y z ≈ x))
90		visset 1810	. . . . . . . . . . . . . . . 16 ⊢ w ∈ V
91		difss 2164	. . . . . . . . . . . . . . . 16 ⊢ (w ∖ {y}) ⊆ w
92	90, 91	ssexi 2716	. . . . . . . . . . . . . . 15 ⊢ (w ∖ {y}) ∈ V
93		psseq1 2132	. . . . . . . . . . . . . . . 16 ⊢ (z = (w ∖ {y}) → (z ⊂ y ↔ (w ∖ {y}) ⊂ y))
94		breq1 2618	. . . . . . . . . . . . . . . . 17 ⊢ (z = (w ∖ {y}) → (z ≈ x ↔ (w ∖ {y}) ≈ x))
95	94	rexbidv 1662	. . . . . . . . . . . . . . . 16 ⊢ (z = (w ∖ {y}) → (∃x ∈ y z ≈ x ↔ ∃x ∈ y (w ∖ {y}) ≈ x))
96	93, 95	imbi12d 625	. . . . . . . . . . . . . . 15 ⊢ (z = (w ∖ {y}) → ((z ⊂ y → ∃x ∈ y z ≈ x) ↔ ((w ∖ {y}) ⊂ y → ∃x ∈ y (w ∖ {y}) ≈ x)))
97	92, 96	cla4v 1865	. . . . . . . . . . . . . 14 ⊢ (∀z(z ⊂ y → ∃x ∈ y z ≈ x) → ((w ∖ {y}) ⊂ y → ∃x ∈ y (w ∖ {y}) ≈ x))
98	89, 97	sylbi 199	. . . . . . . . . . . . 13 ⊢ (∀w(w ⊂ y → ∃x ∈ y w ≈ x) → ((w ∖ {y}) ⊂ y → ∃x ∈ y (w ∖ {y}) ≈ x))
99	84, 98	sylan9 468	. . . . . . . . . . . 12 ⊢ (((y ∈ w ⋀ y ∈ ω) ⋀ ∀w(w ⊂ y → ∃x ∈ y w ≈ x)) → (w ⊂ suc y → ∃x ∈ y (w ∖ {y}) ≈ x))
100		ordsucelsuc 3069	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Ord y → (x ∈ y ↔ suc x ∈ suc y))
101	100	biimpd 153	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Ord y → (x ∈ y → suc x ∈ suc y))
102	58, 101	syl 10	. . . . . . . . . . . . . . . . . . 19 ⊢ (y ∈ ω → (x ∈ y → suc x ∈ suc y))
103	102	adantl 388	. . . . . . . . . . . . . . . . . 18 ⊢ ((y ∈ w ⋀ y ∈ ω) → (x ∈ y → suc x ∈ suc y))
104	103	adantrd 391	. . . . . . . . . . . . . . . . 17 ⊢ ((y ∈ w ⋀ y ∈ ω) → ((x ∈ y ⋀ (w ∖ {y}) ≈ x) → suc x ∈ suc y))
105		difsnid 2464	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (y ∈ w → ((w ∖ {y}) ∪ {y}) = w)
106	105	eqcomd 1478	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (y ∈ w → w = ((w ∖ {y}) ∪ {y}))
107		df-suc 2950	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ suc x = (x ∪ {x})
108	107	a1i 8	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (y ∈ w → suc x = (x ∪ {x}))
109	106, 108	breq12d 2627	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (y ∈ w → (w ≈ suc x ↔ ((w ∖ {y}) ∪ {y}) ≈ (x ∪ {x})))
110		unen 4423	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((w ∖ {y}) ≈ x ⋀ {y} ≈ {x}) ⋀ (((w ∖ {y}) ∩ {y}) = ∅ ⋀ (x ∩ {x}) = ∅)) → ((w ∖ {y}) ∪ {y}) ≈ (x ∪ {x}))
111		visset 1810	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ y ∈ V
112		visset 1810	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ x ∈ V
113	111, 112	f1osn 3714	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {⟨y, x⟩}:{y}–1-1-onto→{x}
114		snex 2746	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ {y} ∈ V
115	114	f1oen 4388	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({⟨y, x⟩}:{y}–1-1-onto→{x} → {y} ≈ {x})
116	113, 115	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {y} ≈ {x}
117	116	jctr 291	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((w ∖ {y}) ≈ x → ((w ∖ {y}) ≈ x ⋀ {y} ≈ {x}))
118		nnord 3136	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (x ∈ ω → Ord x)
119		orddisj 2981	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord x → (x ∩ {x}) = ∅)
120	118, 119	syl 10	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (x ∈ ω → (x ∩ {x}) = ∅)
121		incom 2205	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({y} ∩ (w ∖ {y})) = ((w ∖ {y}) ∩ {y})
122		difdisj 2334	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({y} ∩ (w ∖ {y})) = ∅
123	121, 122	eqtr3 1495	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((w ∖ {y}) ∩ {y}) = ∅
124	120, 123	jctil 292	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (x ∈ ω → (((w ∖ {y}) ∩ {y}) = ∅ ⋀ (x ∩ {x}) = ∅))
125	110, 117, 124	syl2an 454	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((w ∖ {y}) ≈ x ⋀ x ∈ ω) → ((w ∖ {y}) ∪ {y}) ≈ (x ∪ {x}))
126	109, 125	syl5bir 210	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (y ∈ w → (((w ∖ {y}) ≈ x ⋀ x ∈ ω) → w ≈ suc x))
127		elnn 3138	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((x ∈ y ⋀ y ∈ ω) → x ∈ ω)
128	126, 127	sylan2i 465	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y ∈ w → (((w ∖ {y}) ≈ x ⋀ (x ∈ y ⋀ y ∈ ω)) → w ≈ suc x))
129	128	exp4d 381	. . . . . . . . . . . . . . . . . . 19 ⊢ (y ∈ w → ((w ∖ {y}) ≈ x → (x ∈ y → (y ∈ ω → w ≈ suc x))))
130	129	com24 37	. . . . . . . . . . . . . . . . . 18 ⊢ (y ∈ w → (y ∈ ω → (x ∈ y → ((w ∖ {y}) ≈ x → w ≈ suc x))))
131	130	imp4b 365	. . . . . . . . . . . . . . . . 17 ⊢ ((y ∈ w ⋀ y ∈ ω) → ((x ∈ y ⋀ (w ∖ {y}) ≈ x) → w ≈ suc x))
132	104, 131	jcad 599	. . . . . . . . . . . . . . . 16 ⊢ ((y ∈ w ⋀ y ∈ ω) → ((x ∈ y ⋀ (w ∖ {y}) ≈ x) → (suc x ∈ suc y ⋀ w ≈ suc x)))
133		breq2 2619	. . . . . . . . . . . . . . . . 17 ⊢ (z = suc x → (w ≈ z ↔ w ≈ suc x))
134	133	rcla4ev 1874	. . . . . . . . . . . . . . . 16 ⊢ ((suc x ∈ suc y ⋀ w ≈ suc x) → ∃z ∈ suc yw ≈ z)
135	132, 134	syl6 22	. . . . . . . . . . . . . . 15 ⊢ ((y ∈ w ⋀ y ∈ ω) → ((x ∈ y ⋀ (w ∖ {y}) ≈ x) → ∃z ∈ suc yw ≈ z))
136	135	19.23adv 1213	. . . . . . . . . . . . . 14 ⊢ ((y ∈ w ⋀ y ∈ ω) → (∃x(x ∈ y ⋀ (w ∖ {y}) ≈ x) → ∃z ∈ suc yw ≈ z))
137		df-rex 1648	. . . . . . . . . . . . . 14 ⊢ (∃x ∈ y (w ∖ {y}) ≈ x ↔ ∃x(x ∈ y ⋀ (w ∖ {y}) ≈ x))
138		breq2 2619	. . . . . . . . . . . . . . 15 ⊢ (x = z → (w ≈ x ↔ w ≈ z))
139	138	cbvrexv 1798	. . . . . . . . . . . . . 14 ⊢ (∃x ∈ suc yw ≈ x ↔ ∃z ∈ suc yw ≈ z)
140	136, 137, 139	3imtr4g 552	. . . . . . . . . . . . 13 ⊢ ((y ∈ w ⋀ y ∈ ω) → (∃x ∈ y (w ∖ {y}) ≈ x → ∃x ∈ suc yw ≈ x))
141	140	adantr 389	. . . . . . . . . . . 12 ⊢ (((y ∈ w ⋀ y ∈ ω) ⋀ ∀w(w ⊂ y → ∃x ∈ y w ≈ x)) → (∃x ∈ y (w ∖ {y}) ≈ x → ∃x ∈ suc yw ≈ x))
142	99, 141	syld 27	. . . . . . . . . . 11 ⊢ (((y ∈ w ⋀ y ∈ ω) ⋀ ∀w(w ⊂ y → ∃x ∈ y w ≈ x)) → (w ⊂ suc y → ∃x ∈ suc yw ≈ x))
143	142	exp31 376	. . . . . . . . . 10 ⊢ (y ∈ w → (y ∈ ω → (∀w(w ⊂ y → ∃x ∈ y w ≈ x) → (w ⊂ suc y → ∃x ∈ suc yw ≈ x))))
144	143	imp3a 361	. . . . . . . . 9 ⊢ (y ∈ w → ((y ∈ ω ⋀ ∀w(w ⊂ y → ∃x ∈ y w ≈ x)) → (w ⊂ suc y → ∃x ∈ suc yw ≈ x)))
145	90	eqelsuc 3050	. . . . . . . . . . . . 13 ⊢ (w = y → w ∈ suc y)
146	90	enref 4381	. . . . . . . . . . . . 13 ⊢ w ≈ w
147	145, 146	jctir 293	. . . . . . . . . . . 12 ⊢ (w = y → (w ∈ suc y ⋀ w ≈ w))
148		breq2 2619	. . . . . . . . . . . . 13 ⊢ (x = w → (w ≈ x ↔ w ≈ w))
149	148	rcla4ev 1874	. . . . . . . . . . . 12 ⊢ ((w ∈ suc y ⋀ w ≈ w) → ∃x ∈ suc yw ≈ x)
150	147, 149	syl 10	. . . . . . . . . . 11 ⊢ (w = y → ∃x ∈ suc yw ≈ x)
151	150	a1d 12	. . . . . . . . . 10 ⊢ (w = y → (w ⊂ suc y → ∃x ∈ suc yw ≈ x))
152	151	a1d 12	. . . . . . . . 9 ⊢ (w = y → ((y ∈ ω ⋀ ∀w(w ⊂ y → ∃x ∈ y w ≈ x)) → (w ⊂ suc y → ∃x ∈ suc yw ≈ x)))
153	57, 144, 152	pm2.61ii 130	. . . . . . . 8 ⊢ ((y ∈ ω ⋀ ∀w(w ⊂ y → ∃x ∈ y w ≈ x)) → (w ⊂ suc y → ∃x ∈ suc yw ≈ x))
154	153	ex 373	. . . . . . 7 ⊢ (y ∈ ω → (∀w(w ⊂ y → ∃x ∈ y w ≈ x) → (w ⊂ suc y → ∃x ∈ suc yw ≈ x)))
155	29, 30, 154	19.21ad 1058	. . . . . 6 ⊢ (y ∈ ω → (∀w(w ⊂ y → ∃x ∈ y w ≈ x) → ∀w(w ⊂ suc y → ∃x ∈ suc yw ≈ x)))
156	13, 17, 21, 25, 28, 155	finds 3152	. . . . 5 ⊢ (A ∈ ω → ∀w(w ⊂ A → ∃x ∈ A w ≈ x))
157	9, 156	syl5 21	. . . 4 ⊢ (B ∈ V → (A ∈ ω → (B ⊂ A → ∃x ∈ A B ≈ x)))
158	157	com3l 34	. . 3 ⊢ (A ∈ ω → (B ⊂ A → (B ∈ V → ∃x ∈ A B ≈ x)))
159	158	imp 350	. 2 ⊢ ((A ∈ ω ⋀ B ⊂ A) → (B ∈ V → ∃x ∈ A B ≈ x))
160	4, 159	mpd 26	1 ⊢ ((A ∈ ω ⋀ B ⊂ A) → ∃x ∈ A B ≈ x)

Syntax hints:  ¬ wn 2   → wi 3   ⋀ wa 223  ∀wal 953   = wceq 955   ∈ wcel 957  ∃wex 979  ∃wrex 1644  Vcvv 1808   ∖ cdif 2041   ∪ cun 2042   ∩ cin 2043   ⊆ wss 2044   ⊂ wpss 2045  ∅c0 2277  {csn 2406  ⟨cop 2408   class class class wbr 2615  Ord word 2943  suc csuc 2946  ωcom 3127  –1-1-onto→wf1o 3177   ≈ cen 4357

This theorem is referenced by:  ssnn 4523

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-9 964  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458  ax-rep 2689  ax-sep 2699  ax-nul 2706  ax-pow 2738  ax-pr 2775  ax-un 2862

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382  df-clab 1463  df-cleq 1468  df-clel 1471  df-ne 1585  df-ral 1647  df-rex 1648  df-v 1809  df-dif 2046  df-un 2047  df-in 2048  df-ss 2050  df-pss 2052  df-nul 2278  df-if 2359  df-pw 2399  df-sn 2409  df-pr 2410  df-tp 2412  df-op 2413  df-uni 2500  df-br 2616  df-opab 2663  df-tr 2677  df-eprel 2828  df-id 2831  df-po 2836  df-so 2846  df-fr 2913  df-we 2930  df-ord 2947  df-on 2948  df-lim 2949  df-suc 2950  df-om 3128  df-xp 3180  df-rel 3181  df-cnv 3182  df-co 3183  df-dm 3184  df-rn 3185  df-res 3186  df-ima 3187  df-fun 3188  df-fn 3189  df-f 3190  df-f1 3191  df-fo 3192  df-f1o 3193  df-en 4360

Copyright terms: Public domain