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 syl5ibr ( 𝑦 ∈ ω → ( 𝑤 ⊆ suc 𝑦 → ( 𝑤 ∖ { 𝑦 } ) ⊆ 𝑦 ) )
58 30 57 syl5 ( 𝑦 ∈ ω → ( 𝑤 ⊊ suc 𝑦 → ( 𝑤 ∖ { 𝑦 } ) ⊆ 𝑦 ) )
59 pssnel ( 𝑤 ⊊ suc 𝑦 → ∃ 𝑧 ( 𝑧 ∈ suc 𝑦 ∧ ¬ 𝑧𝑤 ) )
60 eleq2 ( ( 𝑤 ∖ { 𝑦 } ) = 𝑦 → ( 𝑧 ∈ ( 𝑤 ∖ { 𝑦 } ) ↔ 𝑧𝑦 ) )
61 eldifi ( 𝑧 ∈ ( 𝑤 ∖ { 𝑦 } ) → 𝑧𝑤 )
62 60 61 syl6bir ( ( 𝑤 ∖ { 𝑦 } ) = 𝑦 → ( 𝑧𝑦𝑧𝑤 ) )
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 syl5bir ( ( 𝑦𝑤𝑦 ∈ ω ) → ( 𝑤 ⊊ suc 𝑦 → ( ( 𝑤 ∖ { 𝑦 } ) ⊆ 𝑦 ∧ ¬ ( 𝑤 ∖ { 𝑦 } ) = 𝑦 ) ) )
75 dfpss2 ( ( 𝑤 ∖ { 𝑦 } ) ⊊ 𝑦 ↔ ( ( 𝑤 ∖ { 𝑦 } ) ⊆ 𝑦 ∧ ¬ ( 𝑤 ∖ { 𝑦 } ) = 𝑦 ) )
76 74 75 syl6ibr ( ( 𝑦𝑤𝑦 ∈ ω ) → ( 𝑤 ⊊ 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 syl5ibr ( 𝑦𝑤 → ( ( ( 𝑤 ∖ { 𝑦 } ) ≈ 𝑥𝑥 ∈ ω ) → 𝑤 ≈ 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 ( ( 𝐴 ∈ ω ∧ 𝐵𝐴 ) → ∃ 𝑥𝐴 𝐵𝑥 )