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
|- ( ( A e. _om /\ B C. A ) -> E. x e. A B ~~ x )

Proof

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