Metamath Proof Explorer

Theorem fin1a2lem9

Description: Lemma for fin1a2 . In a chain of finite sets, initial segments are finite. (Contributed by Stefan O'Rear, 8-Nov-2014)

Ref Expression
Assertion fin1a2lem9 
|- ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) -> { b e. X | b ~<_ A } e. Fin )

Proof

Step Hyp Ref Expression
1 onfin2 
 |-  _om = ( On i^i Fin )
2 inss2 
 |-  ( On i^i Fin ) C_ Fin
3 1 2 eqsstri 
 |-  _om C_ Fin
4 peano2 
 |-  ( A e. _om -> suc A e. _om )
5 3 4 sselid 
 |-  ( A e. _om -> suc A e. Fin )
6 5 3ad2ant3 
 |-  ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) -> suc A e. Fin )
7 4 3ad2ant3 
 |-  ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) -> suc A e. _om )
8 breq1 
 |-  ( b = c -> ( b ~<_ A <-> c ~<_ A ) )
9 8 elrab 
 |-  ( c e. { b e. X | b ~<_ A } <-> ( c e. X /\ c ~<_ A ) )
10 simprr 
 |-  ( ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) /\ ( c e. X /\ c ~<_ A ) ) -> c ~<_ A )
11 simpl2 
 |-  ( ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) /\ ( c e. X /\ c ~<_ A ) ) -> X C_ Fin )
12 simprl 
 |-  ( ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) /\ ( c e. X /\ c ~<_ A ) ) -> c e. X )
13 11 12 sseldd 
 |-  ( ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) /\ ( c e. X /\ c ~<_ A ) ) -> c e. Fin )
14 finnum 
 |-  ( c e. Fin -> c e. dom card )
15 13 14 syl 
 |-  ( ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) /\ ( c e. X /\ c ~<_ A ) ) -> c e. dom card )
16 simpl3 
 |-  ( ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) /\ ( c e. X /\ c ~<_ A ) ) -> A e. _om )
17 3 16 sselid 
 |-  ( ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) /\ ( c e. X /\ c ~<_ A ) ) -> A e. Fin )
18 finnum 
 |-  ( A e. Fin -> A e. dom card )
19 17 18 syl 
 |-  ( ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) /\ ( c e. X /\ c ~<_ A ) ) -> A e. dom card )
20 carddom2 
 |-  ( ( c e. dom card /\ A e. dom card ) -> ( ( card ` c ) C_ ( card ` A ) <-> c ~<_ A ) )
21 15 19 20 syl2anc 
 |-  ( ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) /\ ( c e. X /\ c ~<_ A ) ) -> ( ( card ` c ) C_ ( card ` A ) <-> c ~<_ A ) )
22 10 21 mpbird 
 |-  ( ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) /\ ( c e. X /\ c ~<_ A ) ) -> ( card ` c ) C_ ( card ` A ) )
23 22 ex 
 |-  ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) -> ( ( c e. X /\ c ~<_ A ) -> ( card ` c ) C_ ( card ` A ) ) )
24 cardnn 
 |-  ( A e. _om -> ( card ` A ) = A )
25 24 sseq2d 
 |-  ( A e. _om -> ( ( card ` c ) C_ ( card ` A ) <-> ( card ` c ) C_ A ) )
26 cardon 
 |-  ( card ` c ) e. On
27 nnon 
 |-  ( A e. _om -> A e. On )
28 onsssuc 
 |-  ( ( ( card ` c ) e. On /\ A e. On ) -> ( ( card ` c ) C_ A <-> ( card ` c ) e. suc A ) )
29 26 27 28 sylancr 
 |-  ( A e. _om -> ( ( card ` c ) C_ A <-> ( card ` c ) e. suc A ) )
30 25 29 bitrd 
 |-  ( A e. _om -> ( ( card ` c ) C_ ( card ` A ) <-> ( card ` c ) e. suc A ) )
31 30 3ad2ant3 
 |-  ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) -> ( ( card ` c ) C_ ( card ` A ) <-> ( card ` c ) e. suc A ) )
32 23 31 sylibd 
 |-  ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) -> ( ( c e. X /\ c ~<_ A ) -> ( card ` c ) e. suc A ) )
33 9 32 biimtrid 
 |-  ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) -> ( c e. { b e. X | b ~<_ A } -> ( card ` c ) e. suc A ) )
34 elrabi 
 |-  ( c e. { b e. X | b ~<_ A } -> c e. X )
35 elrabi 
 |-  ( d e. { b e. X | b ~<_ A } -> d e. X )
36 ssel 
 |-  ( X C_ Fin -> ( c e. X -> c e. Fin ) )
37 ssel 
 |-  ( X C_ Fin -> ( d e. X -> d e. Fin ) )
38 36 37 anim12d 
 |-  ( X C_ Fin -> ( ( c e. X /\ d e. X ) -> ( c e. Fin /\ d e. Fin ) ) )
39 38 imp 
 |-  ( ( X C_ Fin /\ ( c e. X /\ d e. X ) ) -> ( c e. Fin /\ d e. Fin ) )
40 39 3ad2antl2 
 |-  ( ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) /\ ( c e. X /\ d e. X ) ) -> ( c e. Fin /\ d e. Fin ) )
41 sorpssi 
 |-  ( ( [C.] Or X /\ ( c e. X /\ d e. X ) ) -> ( c C_ d \/ d C_ c ) )
42 41 3ad2antl1 
 |-  ( ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) /\ ( c e. X /\ d e. X ) ) -> ( c C_ d \/ d C_ c ) )
43 finnum 
 |-  ( d e. Fin -> d e. dom card )
44 carden2 
 |-  ( ( c e. dom card /\ d e. dom card ) -> ( ( card ` c ) = ( card ` d ) <-> c ~~ d ) )
45 14 43 44 syl2an 
 |-  ( ( c e. Fin /\ d e. Fin ) -> ( ( card ` c ) = ( card ` d ) <-> c ~~ d ) )
46 45 adantr 
 |-  ( ( ( c e. Fin /\ d e. Fin ) /\ ( c C_ d \/ d C_ c ) ) -> ( ( card ` c ) = ( card ` d ) <-> c ~~ d ) )
47 fin23lem25 
 |-  ( ( c e. Fin /\ d e. Fin /\ ( c C_ d \/ d C_ c ) ) -> ( c ~~ d <-> c = d ) )
48 47 3expa 
 |-  ( ( ( c e. Fin /\ d e. Fin ) /\ ( c C_ d \/ d C_ c ) ) -> ( c ~~ d <-> c = d ) )
49 48 biimpd 
 |-  ( ( ( c e. Fin /\ d e. Fin ) /\ ( c C_ d \/ d C_ c ) ) -> ( c ~~ d -> c = d ) )
50 46 49 sylbid 
 |-  ( ( ( c e. Fin /\ d e. Fin ) /\ ( c C_ d \/ d C_ c ) ) -> ( ( card ` c ) = ( card ` d ) -> c = d ) )
51 40 42 50 syl2anc 
 |-  ( ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) /\ ( c e. X /\ d e. X ) ) -> ( ( card ` c ) = ( card ` d ) -> c = d ) )
52 fveq2 
 |-  ( c = d -> ( card ` c ) = ( card ` d ) )
53 51 52 impbid1 
 |-  ( ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) /\ ( c e. X /\ d e. X ) ) -> ( ( card ` c ) = ( card ` d ) <-> c = d ) )
54 53 ex 
 |-  ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) -> ( ( c e. X /\ d e. X ) -> ( ( card ` c ) = ( card ` d ) <-> c = d ) ) )
55 34 35 54 syl2ani 
 |-  ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) -> ( ( c e. { b e. X | b ~<_ A } /\ d e. { b e. X | b ~<_ A } ) -> ( ( card ` c ) = ( card ` d ) <-> c = d ) ) )
56 33 55 dom2d 
 |-  ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) -> ( suc A e. _om -> { b e. X | b ~<_ A } ~<_ suc A ) )
57 7 56 mpd 
 |-  ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) -> { b e. X | b ~<_ A } ~<_ suc A )
58 domfi 
 |-  ( ( suc A e. Fin /\ { b e. X | b ~<_ A } ~<_ suc A ) -> { b e. X | b ~<_ A } e. Fin )
59 6 57 58 syl2anc 
 |-  ( ( [C.] Or X /\ X C_ Fin /\ A e. _om ) -> { b e. X | b ~<_ A } e. Fin )