Theorem pssnn 8063

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.)

Assertion

Ref	Expression
pssnn	⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ∃𝑥 ∈ 𝐴 𝐵 ≈ 𝑥)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem pssnn

Dummy variables 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		pssss 3664	. . . 4 ⊢ (𝐵 ⊊ 𝐴 → 𝐵 ⊆ 𝐴)
2		ssexg 4732	. . . 4 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ ω) → 𝐵 ∈ V)
3	1, 2	sylan 487	. . 3 ⊢ ((𝐵 ⊊ 𝐴 ∧ 𝐴 ∈ ω) → 𝐵 ∈ V)
4	3	ancoms 468	. 2 ⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → 𝐵 ∈ V)
5		psseq2 3657	. . . . . . . 8 ⊢ (𝑧 = ∅ → (𝑤 ⊊ 𝑧 ↔ 𝑤 ⊊ ∅))
6		rexeq 3116	. . . . . . . 8 ⊢ (𝑧 = ∅ → (∃𝑥 ∈ 𝑧 𝑤 ≈ 𝑥 ↔ ∃𝑥 ∈ ∅ 𝑤 ≈ 𝑥))
7	5, 6	imbi12d 333	. . . . . . 7 ⊢ (𝑧 = ∅ → ((𝑤 ⊊ 𝑧 → ∃𝑥 ∈ 𝑧 𝑤 ≈ 𝑥) ↔ (𝑤 ⊊ ∅ → ∃𝑥 ∈ ∅ 𝑤 ≈ 𝑥)))
8	7	albidv 1836	. . . . . 6 ⊢ (𝑧 = ∅ → (∀𝑤(𝑤 ⊊ 𝑧 → ∃𝑥 ∈ 𝑧 𝑤 ≈ 𝑥) ↔ ∀𝑤(𝑤 ⊊ ∅ → ∃𝑥 ∈ ∅ 𝑤 ≈ 𝑥)))
9		psseq2 3657	. . . . . . . 8 ⊢ (𝑧 = 𝑦 → (𝑤 ⊊ 𝑧 ↔ 𝑤 ⊊ 𝑦))
10		rexeq 3116	. . . . . . . 8 ⊢ (𝑧 = 𝑦 → (∃𝑥 ∈ 𝑧 𝑤 ≈ 𝑥 ↔ ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥))
11	9, 10	imbi12d 333	. . . . . . 7 ⊢ (𝑧 = 𝑦 → ((𝑤 ⊊ 𝑧 → ∃𝑥 ∈ 𝑧 𝑤 ≈ 𝑥) ↔ (𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥)))
12	11	albidv 1836	. . . . . 6 ⊢ (𝑧 = 𝑦 → (∀𝑤(𝑤 ⊊ 𝑧 → ∃𝑥 ∈ 𝑧 𝑤 ≈ 𝑥) ↔ ∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥)))
13		psseq2 3657	. . . . . . . 8 ⊢ (𝑧 = suc 𝑦 → (𝑤 ⊊ 𝑧 ↔ 𝑤 ⊊ suc 𝑦))
14		rexeq 3116	. . . . . . . 8 ⊢ (𝑧 = suc 𝑦 → (∃𝑥 ∈ 𝑧 𝑤 ≈ 𝑥 ↔ ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥))
15	13, 14	imbi12d 333	. . . . . . 7 ⊢ (𝑧 = suc 𝑦 → ((𝑤 ⊊ 𝑧 → ∃𝑥 ∈ 𝑧 𝑤 ≈ 𝑥) ↔ (𝑤 ⊊ suc 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥)))
16	15	albidv 1836	. . . . . 6 ⊢ (𝑧 = suc 𝑦 → (∀𝑤(𝑤 ⊊ 𝑧 → ∃𝑥 ∈ 𝑧 𝑤 ≈ 𝑥) ↔ ∀𝑤(𝑤 ⊊ suc 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥)))
17		psseq2 3657	. . . . . . . 8 ⊢ (𝑧 = 𝐴 → (𝑤 ⊊ 𝑧 ↔ 𝑤 ⊊ 𝐴))
18		rexeq 3116	. . . . . . . 8 ⊢ (𝑧 = 𝐴 → (∃𝑥 ∈ 𝑧 𝑤 ≈ 𝑥 ↔ ∃𝑥 ∈ 𝐴 𝑤 ≈ 𝑥))
19	17, 18	imbi12d 333	. . . . . . 7 ⊢ (𝑧 = 𝐴 → ((𝑤 ⊊ 𝑧 → ∃𝑥 ∈ 𝑧 𝑤 ≈ 𝑥) ↔ (𝑤 ⊊ 𝐴 → ∃𝑥 ∈ 𝐴 𝑤 ≈ 𝑥)))
20	19	albidv 1836	. . . . . 6 ⊢ (𝑧 = 𝐴 → (∀𝑤(𝑤 ⊊ 𝑧 → ∃𝑥 ∈ 𝑧 𝑤 ≈ 𝑥) ↔ ∀𝑤(𝑤 ⊊ 𝐴 → ∃𝑥 ∈ 𝐴 𝑤 ≈ 𝑥)))
21		npss0 3966	. . . . . . . 8 ⊢ ¬ 𝑤 ⊊ ∅
22	21	pm2.21i 115	. . . . . . 7 ⊢ (𝑤 ⊊ ∅ → ∃𝑥 ∈ ∅ 𝑤 ≈ 𝑥)
23	22	ax-gen 1713	. . . . . 6 ⊢ ∀𝑤(𝑤 ⊊ ∅ → ∃𝑥 ∈ ∅ 𝑤 ≈ 𝑥)
24		nfv 1830	. . . . . . 7 ⊢ Ⅎ𝑤 𝑦 ∈ ω
25		nfa1 2015	. . . . . . 7 ⊢ Ⅎ𝑤∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥)
26		elequ1 1984	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝑤 ↔ 𝑦 ∈ 𝑤))
27	26	biimpcd 238	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ 𝑤 → (𝑧 = 𝑦 → 𝑦 ∈ 𝑤))
28	27	con3d 147	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ 𝑤 → (¬ 𝑦 ∈ 𝑤 → ¬ 𝑧 = 𝑦))
29	28	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤 ⊊ suc 𝑦 ∧ 𝑧 ∈ 𝑤) → (¬ 𝑦 ∈ 𝑤 → ¬ 𝑧 = 𝑦))
30		pssss 3664	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ⊊ suc 𝑦 → 𝑤 ⊆ suc 𝑦)
31	30	sseld 3567	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ⊊ suc 𝑦 → (𝑧 ∈ 𝑤 → 𝑧 ∈ suc 𝑦))
32		elsuci 5708	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ suc 𝑦 → (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦))
33	32	ord 391	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ suc 𝑦 → (¬ 𝑧 ∈ 𝑦 → 𝑧 = 𝑦))
34	33	con1d 138	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ suc 𝑦 → (¬ 𝑧 = 𝑦 → 𝑧 ∈ 𝑦))
35	31, 34	syl6 34	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ⊊ suc 𝑦 → (𝑧 ∈ 𝑤 → (¬ 𝑧 = 𝑦 → 𝑧 ∈ 𝑦)))
36	35	imp 444	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤 ⊊ suc 𝑦 ∧ 𝑧 ∈ 𝑤) → (¬ 𝑧 = 𝑦 → 𝑧 ∈ 𝑦))
37	29, 36	syld 46	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 ⊊ suc 𝑦 ∧ 𝑧 ∈ 𝑤) → (¬ 𝑦 ∈ 𝑤 → 𝑧 ∈ 𝑦))
38	37	impancom 455	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ⊊ suc 𝑦 ∧ ¬ 𝑦 ∈ 𝑤) → (𝑧 ∈ 𝑤 → 𝑧 ∈ 𝑦))
39	38	ssrdv 3574	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ⊊ suc 𝑦 ∧ ¬ 𝑦 ∈ 𝑤) → 𝑤 ⊆ 𝑦)
40	39	anim1i 590	. . . . . . . . . . . . . . 15 ⊢ (((𝑤 ⊊ suc 𝑦 ∧ ¬ 𝑦 ∈ 𝑤) ∧ ¬ 𝑤 = 𝑦) → (𝑤 ⊆ 𝑦 ∧ ¬ 𝑤 = 𝑦))
41		dfpss2 3654	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ⊊ 𝑦 ↔ (𝑤 ⊆ 𝑦 ∧ ¬ 𝑤 = 𝑦))
42	40, 41	sylibr 223	. . . . . . . . . . . . . 14 ⊢ (((𝑤 ⊊ suc 𝑦 ∧ ¬ 𝑦 ∈ 𝑤) ∧ ¬ 𝑤 = 𝑦) → 𝑤 ⊊ 𝑦)
43		elelsuc 5714	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝑦 → 𝑥 ∈ suc 𝑦)
44	43	anim1i 590	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑤 ≈ 𝑥) → (𝑥 ∈ suc 𝑦 ∧ 𝑤 ≈ 𝑥))
45	44	reximi2 2993	. . . . . . . . . . . . . 14 ⊢ (∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥)
46	42, 45	imim12i 60	. . . . . . . . . . . . 13 ⊢ ((𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥) → (((𝑤 ⊊ suc 𝑦 ∧ ¬ 𝑦 ∈ 𝑤) ∧ ¬ 𝑤 = 𝑦) → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥))
47	46	exp4c 634	. . . . . . . . . . . 12 ⊢ ((𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥) → (𝑤 ⊊ suc 𝑦 → (¬ 𝑦 ∈ 𝑤 → (¬ 𝑤 = 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥))))
48	47	sps 2043	. . . . . . . . . . 11 ⊢ (∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥) → (𝑤 ⊊ suc 𝑦 → (¬ 𝑦 ∈ 𝑤 → (¬ 𝑤 = 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥))))
49	48	adantl 481	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥)) → (𝑤 ⊊ suc 𝑦 → (¬ 𝑦 ∈ 𝑤 → (¬ 𝑤 = 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥))))
50	49	com4t 91	. . . . . . . . 9 ⊢ (¬ 𝑦 ∈ 𝑤 → (¬ 𝑤 = 𝑦 → ((𝑦 ∈ ω ∧ ∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥)) → (𝑤 ⊊ suc 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥))))
51		anidm 674	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ⊊ suc 𝑦 ∧ 𝑤 ⊊ suc 𝑦) ↔ 𝑤 ⊊ suc 𝑦)
52		ssdif 3707	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ⊆ suc 𝑦 → (𝑤 ∖ {𝑦}) ⊆ (suc 𝑦 ∖ {𝑦}))
53		nnord 6965	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ω → Ord 𝑦)
54		orddif 5737	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord 𝑦 → 𝑦 = (suc 𝑦 ∖ {𝑦}))
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ω → 𝑦 = (suc 𝑦 ∖ {𝑦}))
56	55	sseq2d 3596	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ω → ((𝑤 ∖ {𝑦}) ⊆ 𝑦 ↔ (𝑤 ∖ {𝑦}) ⊆ (suc 𝑦 ∖ {𝑦})))
57	52, 56	syl5ibr 235	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ω → (𝑤 ⊆ suc 𝑦 → (𝑤 ∖ {𝑦}) ⊆ 𝑦))
58	30, 57	syl5 33	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ω → (𝑤 ⊊ suc 𝑦 → (𝑤 ∖ {𝑦}) ⊆ 𝑦))
59		pssnel 3991	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ⊊ suc 𝑦 → ∃𝑧(𝑧 ∈ suc 𝑦 ∧ ¬ 𝑧 ∈ 𝑤))
60		eleq2 2677	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑤 ∖ {𝑦}) = 𝑦 → (𝑧 ∈ (𝑤 ∖ {𝑦}) ↔ 𝑧 ∈ 𝑦))
61		eldifi 3694	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ (𝑤 ∖ {𝑦}) → 𝑧 ∈ 𝑤)
62	60, 61	syl6bir 243	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑤 ∖ {𝑦}) = 𝑦 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑤))
63	62	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑦 ∈ 𝑤 ∧ 𝑧 ∈ suc 𝑦) ∧ (𝑤 ∖ {𝑦}) = 𝑦) → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑤))
64		eleq1a 2683	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ 𝑤 → (𝑧 = 𝑦 → 𝑧 ∈ 𝑤))
65	33, 64	sylan9r 688	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ 𝑤 ∧ 𝑧 ∈ suc 𝑦) → (¬ 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑤))
66	65	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑦 ∈ 𝑤 ∧ 𝑧 ∈ suc 𝑦) ∧ (𝑤 ∖ {𝑦}) = 𝑦) → (¬ 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑤))
67	63, 66	pm2.61d 169	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ∈ 𝑤 ∧ 𝑧 ∈ suc 𝑦) ∧ (𝑤 ∖ {𝑦}) = 𝑦) → 𝑧 ∈ 𝑤)
68	67	ex 449	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ 𝑤 ∧ 𝑧 ∈ suc 𝑦) → ((𝑤 ∖ {𝑦}) = 𝑦 → 𝑧 ∈ 𝑤))
69	68	con3d 147	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ 𝑤 ∧ 𝑧 ∈ suc 𝑦) → (¬ 𝑧 ∈ 𝑤 → ¬ (𝑤 ∖ {𝑦}) = 𝑦))
70	69	expimpd 627	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ 𝑤 → ((𝑧 ∈ suc 𝑦 ∧ ¬ 𝑧 ∈ 𝑤) → ¬ (𝑤 ∖ {𝑦}) = 𝑦))
71	70	exlimdv 1848	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝑤 → (∃𝑧(𝑧 ∈ suc 𝑦 ∧ ¬ 𝑧 ∈ 𝑤) → ¬ (𝑤 ∖ {𝑦}) = 𝑦))
72	59, 71	syl5 33	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝑤 → (𝑤 ⊊ suc 𝑦 → ¬ (𝑤 ∖ {𝑦}) = 𝑦))
73	58, 72	im2anan9r 877	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) → ((𝑤 ⊊ suc 𝑦 ∧ 𝑤 ⊊ suc 𝑦) → ((𝑤 ∖ {𝑦}) ⊆ 𝑦 ∧ ¬ (𝑤 ∖ {𝑦}) = 𝑦)))
74	51, 73	syl5bir 232	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) → (𝑤 ⊊ suc 𝑦 → ((𝑤 ∖ {𝑦}) ⊆ 𝑦 ∧ ¬ (𝑤 ∖ {𝑦}) = 𝑦)))
75		dfpss2 3654	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∖ {𝑦}) ⊊ 𝑦 ↔ ((𝑤 ∖ {𝑦}) ⊆ 𝑦 ∧ ¬ (𝑤 ∖ {𝑦}) = 𝑦))
76	74, 75	syl6ibr 241	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) → (𝑤 ⊊ suc 𝑦 → (𝑤 ∖ {𝑦}) ⊊ 𝑦))
77		psseq1 3656	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑧 → (𝑤 ⊊ 𝑦 ↔ 𝑧 ⊊ 𝑦))
78		breq1 4586	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑧 → (𝑤 ≈ 𝑥 ↔ 𝑧 ≈ 𝑥))
79	78	rexbidv 3034	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑧 → (∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥 ↔ ∃𝑥 ∈ 𝑦 𝑧 ≈ 𝑥))
80	77, 79	imbi12d 333	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑧 → ((𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥) ↔ (𝑧 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑧 ≈ 𝑥)))
81	80	cbvalv 2261	. . . . . . . . . . . . 13 ⊢ (∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥) ↔ ∀𝑧(𝑧 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑧 ≈ 𝑥))
82		vex 3176	. . . . . . . . . . . . . . 15 ⊢ 𝑤 ∈ V
83		difss 3699	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∖ {𝑦}) ⊆ 𝑤
84	82, 83	ssexi 4731	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∖ {𝑦}) ∈ V
85		psseq1 3656	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑤 ∖ {𝑦}) → (𝑧 ⊊ 𝑦 ↔ (𝑤 ∖ {𝑦}) ⊊ 𝑦))
86		breq1 4586	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑤 ∖ {𝑦}) → (𝑧 ≈ 𝑥 ↔ (𝑤 ∖ {𝑦}) ≈ 𝑥))
87	86	rexbidv 3034	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑤 ∖ {𝑦}) → (∃𝑥 ∈ 𝑦 𝑧 ≈ 𝑥 ↔ ∃𝑥 ∈ 𝑦 (𝑤 ∖ {𝑦}) ≈ 𝑥))
88	85, 87	imbi12d 333	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑤 ∖ {𝑦}) → ((𝑧 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑧 ≈ 𝑥) ↔ ((𝑤 ∖ {𝑦}) ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 (𝑤 ∖ {𝑦}) ≈ 𝑥)))
89	84, 88	spcv 3272	. . . . . . . . . . . . 13 ⊢ (∀𝑧(𝑧 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑧 ≈ 𝑥) → ((𝑤 ∖ {𝑦}) ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 (𝑤 ∖ {𝑦}) ≈ 𝑥))
90	81, 89	sylbi 206	. . . . . . . . . . . 12 ⊢ (∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥) → ((𝑤 ∖ {𝑦}) ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 (𝑤 ∖ {𝑦}) ≈ 𝑥))
91	76, 90	sylan9 687	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) ∧ ∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥)) → (𝑤 ⊊ suc 𝑦 → ∃𝑥 ∈ 𝑦 (𝑤 ∖ {𝑦}) ≈ 𝑥))
92		ordsucelsuc 6914	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Ord 𝑦 → (𝑥 ∈ 𝑦 ↔ suc 𝑥 ∈ suc 𝑦))
93	92	biimpd 218	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord 𝑦 → (𝑥 ∈ 𝑦 → suc 𝑥 ∈ suc 𝑦))
94	53, 93	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ω → (𝑥 ∈ 𝑦 → suc 𝑥 ∈ suc 𝑦))
95	94	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) → (𝑥 ∈ 𝑦 → suc 𝑥 ∈ suc 𝑦))
96	95	adantrd 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) → ((𝑥 ∈ 𝑦 ∧ (𝑤 ∖ {𝑦}) ≈ 𝑥) → suc 𝑥 ∈ suc 𝑦))
97		elnn 6967	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ω) → 𝑥 ∈ ω)
98		snex 4835	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {⟨𝑦, 𝑥⟩} ∈ V
99		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑦 ∈ V
100		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑥 ∈ V
101	99, 100	f1osn 6088	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {⟨𝑦, 𝑥⟩}:{𝑦}–1-1-onto→{𝑥}
102		f1oen3g 7857	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (({⟨𝑦, 𝑥⟩} ∈ V ∧ {⟨𝑦, 𝑥⟩}:{𝑦}–1-1-onto→{𝑥}) → {𝑦} ≈ {𝑥})
103	98, 101, 102	mp2an 704	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑦} ≈ {𝑥}
104	103	jctr 563	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑤 ∖ {𝑦}) ≈ 𝑥 → ((𝑤 ∖ {𝑦}) ≈ 𝑥 ∧ {𝑦} ≈ {𝑥}))
105		nnord 6965	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ω → Ord 𝑥)
106		orddisj 5679	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Ord 𝑥 → (𝑥 ∩ {𝑥}) = ∅)
107	105, 106	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ω → (𝑥 ∩ {𝑥}) = ∅)
108		incom 3767	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ({𝑦} ∩ (𝑤 ∖ {𝑦})) = ((𝑤 ∖ {𝑦}) ∩ {𝑦})
109		disjdif 3992	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ({𝑦} ∩ (𝑤 ∖ {𝑦})) = ∅
110	108, 109	eqtr3i 2634	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑤 ∖ {𝑦}) ∩ {𝑦}) = ∅
111	107, 110	jctil 558	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ω → (((𝑤 ∖ {𝑦}) ∩ {𝑦}) = ∅ ∧ (𝑥 ∩ {𝑥}) = ∅))
112		unen 7925	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑤 ∖ {𝑦}) ≈ 𝑥 ∧ {𝑦} ≈ {𝑥}) ∧ (((𝑤 ∖ {𝑦}) ∩ {𝑦}) = ∅ ∧ (𝑥 ∩ {𝑥}) = ∅)) → ((𝑤 ∖ {𝑦}) ∪ {𝑦}) ≈ (𝑥 ∪ {𝑥}))
113	104, 111, 112	syl2an 493	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑤 ∖ {𝑦}) ≈ 𝑥 ∧ 𝑥 ∈ ω) → ((𝑤 ∖ {𝑦}) ∪ {𝑦}) ≈ (𝑥 ∪ {𝑥}))
114		difsnid 4282	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ 𝑤 → ((𝑤 ∖ {𝑦}) ∪ {𝑦}) = 𝑤)
115	114	eqcomd 2616	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ 𝑤 → 𝑤 = ((𝑤 ∖ {𝑦}) ∪ {𝑦}))
116		df-suc 5646	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ suc 𝑥 = (𝑥 ∪ {𝑥})
117	116	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ 𝑤 → suc 𝑥 = (𝑥 ∪ {𝑥}))
118	115, 117	breq12d 4596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ 𝑤 → (𝑤 ≈ suc 𝑥 ↔ ((𝑤 ∖ {𝑦}) ∪ {𝑦}) ≈ (𝑥 ∪ {𝑥})))
119	113, 118	syl5ibr 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ 𝑤 → (((𝑤 ∖ {𝑦}) ≈ 𝑥 ∧ 𝑥 ∈ ω) → 𝑤 ≈ suc 𝑥))
120	97, 119	sylan2i 685	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝑤 → (((𝑤 ∖ {𝑦}) ≈ 𝑥 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ω)) → 𝑤 ≈ suc 𝑥))
121	120	exp4d 635	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ 𝑤 → ((𝑤 ∖ {𝑦}) ≈ 𝑥 → (𝑥 ∈ 𝑦 → (𝑦 ∈ ω → 𝑤 ≈ suc 𝑥))))
122	121	com24 93	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ 𝑤 → (𝑦 ∈ ω → (𝑥 ∈ 𝑦 → ((𝑤 ∖ {𝑦}) ≈ 𝑥 → 𝑤 ≈ suc 𝑥))))
123	122	imp4b 611	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) → ((𝑥 ∈ 𝑦 ∧ (𝑤 ∖ {𝑦}) ≈ 𝑥) → 𝑤 ≈ suc 𝑥))
124	96, 123	jcad 554	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) → ((𝑥 ∈ 𝑦 ∧ (𝑤 ∖ {𝑦}) ≈ 𝑥) → (suc 𝑥 ∈ suc 𝑦 ∧ 𝑤 ≈ suc 𝑥)))
125		breq2 4587	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = suc 𝑥 → (𝑤 ≈ 𝑧 ↔ 𝑤 ≈ suc 𝑥))
126	125	rspcev 3282	. . . . . . . . . . . . . . 15 ⊢ ((suc 𝑥 ∈ suc 𝑦 ∧ 𝑤 ≈ suc 𝑥) → ∃𝑧 ∈ suc 𝑦𝑤 ≈ 𝑧)
127	124, 126	syl6 34	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) → ((𝑥 ∈ 𝑦 ∧ (𝑤 ∖ {𝑦}) ≈ 𝑥) → ∃𝑧 ∈ suc 𝑦𝑤 ≈ 𝑧))
128	127	exlimdv 1848	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) → (∃𝑥(𝑥 ∈ 𝑦 ∧ (𝑤 ∖ {𝑦}) ≈ 𝑥) → ∃𝑧 ∈ suc 𝑦𝑤 ≈ 𝑧))
129		df-rex 2902	. . . . . . . . . . . . 13 ⊢ (∃𝑥 ∈ 𝑦 (𝑤 ∖ {𝑦}) ≈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ (𝑤 ∖ {𝑦}) ≈ 𝑥))
130		breq2 4587	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → (𝑤 ≈ 𝑥 ↔ 𝑤 ≈ 𝑧))
131	130	cbvrexv 3148	. . . . . . . . . . . . 13 ⊢ (∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥 ↔ ∃𝑧 ∈ suc 𝑦𝑤 ≈ 𝑧)
132	128, 129, 131	3imtr4g 284	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) → (∃𝑥 ∈ 𝑦 (𝑤 ∖ {𝑦}) ≈ 𝑥 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥))
133	132	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) ∧ ∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥)) → (∃𝑥 ∈ 𝑦 (𝑤 ∖ {𝑦}) ≈ 𝑥 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥))
134	91, 133	syld 46	. . . . . . . . . 10 ⊢ (((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) ∧ ∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥)) → (𝑤 ⊊ suc 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥))
135	134	expl 646	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝑤 → ((𝑦 ∈ ω ∧ ∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥)) → (𝑤 ⊊ suc 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥)))
136	82	eqelsuc 5723	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑦 → 𝑤 ∈ suc 𝑦)
137	82	enref 7874	. . . . . . . . . . 11 ⊢ 𝑤 ≈ 𝑤
138		breq2 4587	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (𝑤 ≈ 𝑥 ↔ 𝑤 ≈ 𝑤))
139	138	rspcev 3282	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ suc 𝑦 ∧ 𝑤 ≈ 𝑤) → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥)
140	136, 137, 139	sylancl 693	. . . . . . . . . 10 ⊢ (𝑤 = 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥)
141	140	2a1d 26	. . . . . . . . 9 ⊢ (𝑤 = 𝑦 → ((𝑦 ∈ ω ∧ ∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥)) → (𝑤 ⊊ suc 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥)))
142	50, 135, 141	pm2.61ii 176	. . . . . . . 8 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥)) → (𝑤 ⊊ suc 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥))
143	142	ex 449	. . . . . . 7 ⊢ (𝑦 ∈ ω → (∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥) → (𝑤 ⊊ suc 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥)))
144	24, 25, 143	alrimd 2071	. . . . . 6 ⊢ (𝑦 ∈ ω → (∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥) → ∀𝑤(𝑤 ⊊ suc 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥)))
145	8, 12, 16, 20, 23, 144	finds 6984	. . . . 5 ⊢ (𝐴 ∈ ω → ∀𝑤(𝑤 ⊊ 𝐴 → ∃𝑥 ∈ 𝐴 𝑤 ≈ 𝑥))
146		psseq1 3656	. . . . . . 7 ⊢ (𝑤 = 𝐵 → (𝑤 ⊊ 𝐴 ↔ 𝐵 ⊊ 𝐴))
147		breq1 4586	. . . . . . . 8 ⊢ (𝑤 = 𝐵 → (𝑤 ≈ 𝑥 ↔ 𝐵 ≈ 𝑥))
148	147	rexbidv 3034	. . . . . . 7 ⊢ (𝑤 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑤 ≈ 𝑥 ↔ ∃𝑥 ∈ 𝐴 𝐵 ≈ 𝑥))
149	146, 148	imbi12d 333	. . . . . 6 ⊢ (𝑤 = 𝐵 → ((𝑤 ⊊ 𝐴 → ∃𝑥 ∈ 𝐴 𝑤 ≈ 𝑥) ↔ (𝐵 ⊊ 𝐴 → ∃𝑥 ∈ 𝐴 𝐵 ≈ 𝑥)))
150	149	spcgv 3266	. . . . 5 ⊢ (𝐵 ∈ V → (∀𝑤(𝑤 ⊊ 𝐴 → ∃𝑥 ∈ 𝐴 𝑤 ≈ 𝑥) → (𝐵 ⊊ 𝐴 → ∃𝑥 ∈ 𝐴 𝐵 ≈ 𝑥)))
151	145, 150	syl5 33	. . . 4 ⊢ (𝐵 ∈ V → (𝐴 ∈ ω → (𝐵 ⊊ 𝐴 → ∃𝑥 ∈ 𝐴 𝐵 ≈ 𝑥)))
152	151	com3l 87	. . 3 ⊢ (𝐴 ∈ ω → (𝐵 ⊊ 𝐴 → (𝐵 ∈ V → ∃𝑥 ∈ 𝐴 𝐵 ≈ 𝑥)))
153	152	imp 444	. 2 ⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → (𝐵 ∈ V → ∃𝑥 ∈ 𝐴 𝐵 ≈ 𝑥))
154	4, 153	mpd 15	1 ⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ∃𝑥 ∈ 𝐴 𝐵 ≈ 𝑥)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977  ∃wrex 2897  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540   ⊊ wpss 3541  ∅c0 3874  {csn 4125  ⟨cop 4131   class class class wbr 4583  Ord word 5639  suc csuc 5642  –1-1-onto→wf1o 5803  ωcom 6957   ≈ cen 7838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-om 6958  df-en 7842

This theorem is referenced by:  ssnnfi  8064