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 
|- ( ( 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 imbitrrid 
 |-  ( 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 biimtrrdi 
 |-  ( ( 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 biimtrrid 
 |-  ( ( 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 imbitrrdi 
 |-  ( ( 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 imbitrrid 
 |-  ( 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 )