Metamath Proof Explorer

Theorem isfin4p1

Description: Alternate definition of IV-finite sets: they are strictly dominated by their successors. (Thus, the proper subset referred to in isfin4 can be assumed to be only a singleton smaller than the original.) (Contributed by Mario Carneiro, 18-May-2015)

Ref Expression
Assertion isfin4p1 
|- ( A e. Fin4 <-> A ~< ( A |_| 1o ) )

Proof

Step Hyp Ref Expression
1 1on 
 |-  1o e. On
2 djudoml 
 |-  ( ( A e. Fin4 /\ 1o e. On ) -> A ~<_ ( A |_| 1o ) )
3 1 2 mpan2 
 |-  ( A e. Fin4 -> A ~<_ ( A |_| 1o ) )
4 1oex 
 |-  1o e. _V
5 4 snid 
 |-  1o e. { 1o }
6 0lt1o 
 |-  (/) e. 1o
7 opelxpi 
 |-  ( ( 1o e. { 1o } /\ (/) e. 1o ) -> <. 1o , (/) >. e. ( { 1o } X. 1o ) )
8 5 6 7 mp2an 
 |-  <. 1o , (/) >. e. ( { 1o } X. 1o )
9 elun2 
 |-  ( <. 1o , (/) >. e. ( { 1o } X. 1o ) -> <. 1o , (/) >. e. ( ( { (/) } X. A ) u. ( { 1o } X. 1o ) ) )
10 8 9 ax-mp 
 |-  <. 1o , (/) >. e. ( ( { (/) } X. A ) u. ( { 1o } X. 1o ) )
11 df-dju 
 |-  ( A |_| 1o ) = ( ( { (/) } X. A ) u. ( { 1o } X. 1o ) )
12 10 11 eleqtrri 
 |-  <. 1o , (/) >. e. ( A |_| 1o )
13 1n0 
 |-  1o =/= (/)
14 opelxp1 
 |-  ( <. 1o , (/) >. e. ( { (/) } X. A ) -> 1o e. { (/) } )
15 elsni 
 |-  ( 1o e. { (/) } -> 1o = (/) )
16 14 15 syl 
 |-  ( <. 1o , (/) >. e. ( { (/) } X. A ) -> 1o = (/) )
17 16 necon3ai 
 |-  ( 1o =/= (/) -> -. <. 1o , (/) >. e. ( { (/) } X. A ) )
18 13 17 ax-mp 
 |-  -. <. 1o , (/) >. e. ( { (/) } X. A )
19 ssun1 
 |-  ( { (/) } X. A ) C_ ( ( { (/) } X. A ) u. ( { 1o } X. 1o ) )
20 19 11 sseqtrri 
 |-  ( { (/) } X. A ) C_ ( A |_| 1o )
21 ssnelpss 
 |-  ( ( { (/) } X. A ) C_ ( A |_| 1o ) -> ( ( <. 1o , (/) >. e. ( A |_| 1o ) /\ -. <. 1o , (/) >. e. ( { (/) } X. A ) ) -> ( { (/) } X. A ) C. ( A |_| 1o ) ) )
22 20 21 ax-mp 
 |-  ( ( <. 1o , (/) >. e. ( A |_| 1o ) /\ -. <. 1o , (/) >. e. ( { (/) } X. A ) ) -> ( { (/) } X. A ) C. ( A |_| 1o ) )
23 12 18 22 mp2an 
 |-  ( { (/) } X. A ) C. ( A |_| 1o )
24 0ex 
 |-  (/) e. _V
25 relen 
 |-  Rel ~~
26 25 brrelex1i 
 |-  ( A ~~ ( A |_| 1o ) -> A e. _V )
27 xpsnen2g 
 |-  ( ( (/) e. _V /\ A e. _V ) -> ( { (/) } X. A ) ~~ A )
28 24 26 27 sylancr 
 |-  ( A ~~ ( A |_| 1o ) -> ( { (/) } X. A ) ~~ A )
29 entr 
 |-  ( ( ( { (/) } X. A ) ~~ A /\ A ~~ ( A |_| 1o ) ) -> ( { (/) } X. A ) ~~ ( A |_| 1o ) )
30 28 29 mpancom 
 |-  ( A ~~ ( A |_| 1o ) -> ( { (/) } X. A ) ~~ ( A |_| 1o ) )
31 fin4i 
 |-  ( ( ( { (/) } X. A ) C. ( A |_| 1o ) /\ ( { (/) } X. A ) ~~ ( A |_| 1o ) ) -> -. ( A |_| 1o ) e. Fin4 )
32 23 30 31 sylancr 
 |-  ( A ~~ ( A |_| 1o ) -> -. ( A |_| 1o ) e. Fin4 )
33 fin4en1 
 |-  ( A ~~ ( A |_| 1o ) -> ( A e. Fin4 -> ( A |_| 1o ) e. Fin4 ) )
34 32 33 mtod 
 |-  ( A ~~ ( A |_| 1o ) -> -. A e. Fin4 )
35 34 con2i 
 |-  ( A e. Fin4 -> -. A ~~ ( A |_| 1o ) )
36 brsdom 
 |-  ( A ~< ( A |_| 1o ) <-> ( A ~<_ ( A |_| 1o ) /\ -. A ~~ ( A |_| 1o ) ) )
37 3 35 36 sylanbrc 
 |-  ( A e. Fin4 -> A ~< ( A |_| 1o ) )
38 sdomnen 
 |-  ( A ~< ( A |_| 1o ) -> -. A ~~ ( A |_| 1o ) )
39 infdju1 
 |-  ( _om ~<_ A -> ( A |_| 1o ) ~~ A )
40 39 ensymd 
 |-  ( _om ~<_ A -> A ~~ ( A |_| 1o ) )
41 38 40 nsyl 
 |-  ( A ~< ( A |_| 1o ) -> -. _om ~<_ A )
42 relsdom 
 |-  Rel ~<
43 42 brrelex1i 
 |-  ( A ~< ( A |_| 1o ) -> A e. _V )
44 isfin4-2 
 |-  ( A e. _V -> ( A e. Fin4 <-> -. _om ~<_ A ) )
45 43 44 syl 
 |-  ( A ~< ( A |_| 1o ) -> ( A e. Fin4 <-> -. _om ~<_ A ) )
46 41 45 mpbird 
 |-  ( A ~< ( A |_| 1o ) -> A e. Fin4 )
47 37 46 impbii 
 |-  ( A e. Fin4 <-> A ~< ( A |_| 1o ) )