This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ( ( 𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 𝐵 ≈ 𝑥 )

Proof

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