Step Hyp Ref
Expression 1 df-ne 2654 . . . . 5
2 simplr 755 . . . . . . . . . 10
3 simpll 753 . . . . . . . . . 10
4 onwf 8269 . . . . . . . . . . . . . . . 16
5 4 sseli 3499 . . . . . . . . . . . . . . 15
6 eqid 2457 . . . . . . . . . . . . . . . 16
7 rankr1c 8260 . . . . . . . . . . . . . . . 16
8 6 , 7 mpbii 211 . . . . . . . . . . . . . . 15
9 5 , 8 syl 16 . . . . . . . . . . . . . 14
10 9 simpld 459 . . . . . . . . . . . . 13
11 r1fnon 8206 . . . . . . . . . . . . . . . . 17
12 fndm 5685 . . . . . . . . . . . . . . . . 17
13 11 , 12 ax-mp 5 . . . . . . . . . . . . . . . 16
14 13 eleq2i 2535 . . . . . . . . . . . . . . 15
15 rankonid 8268 . . . . . . . . . . . . . . 15
16 14 , 15 bitr3i 251 . . . . . . . . . . . . . 14
17 fveq2 5871 . . . . . . . . . . . . . 14
18 16 , 17 sylbi 195 . . . . . . . . . . . . 13
19 10 , 18 neleqtrd 2569 . . . . . . . . . . . 12
20 19 adantl 466 . . . . . . . . . . 11
21 onssr1 8270 . . . . . . . . . . . . . 14
22 14 , 21 sylbir 213 . . . . . . . . . . . . 13
23 tsken 9153 . . . . . . . . . . . . 13
24 22 , 23 sylan2 474 . . . . . . . . . . . 12
25 24 ord 377 . . . . . . . . . . 11
26 20 , 25 mt3d 125 . . . . . . . . . 10
27 2 , 3 , 26 syl2anc 661 . . . . . . . . 9
28 carden2b 8369 . . . . . . . . 9
29 27 , 28 syl 16 . . . . . . . 8
30 simpl 457 . . . . . . . . . 10
31 simplr 755 . . . . . . . . . . . . 13
32 22 adantr 465 . . . . . . . . . . . . . 14
33 32 sselda 3503 . . . . . . . . . . . . 13
34 tsksdom 9155 . . . . . . . . . . . . 13
35 31 , 33 , 34 syl2anc 661 . . . . . . . . . . . 12
36 simpll 753 . . . . . . . . . . . . 13
37 26 ensymd 7586 . . . . . . . . . . . . 13
38 31 , 36 , 37 syl2anc 661 . . . . . . . . . . . 12
39 sdomentr 7671 . . . . . . . . . . . 12
40 35 , 38 , 39 syl2anc 661 . . . . . . . . . . 11
41 40 ralrimiva 2871 . . . . . . . . . 10
42 iscard 8377 . . . . . . . . . 10
43 30 , 41 , 42 sylanbrc 664 . . . . . . . . 9
44 43 adantr 465 . . . . . . . 8
45 29 , 44 eqtr3d 2500 . . . . . . 7
46 r10 8207 . . . . . . . . . . 11
47 on0eln0 4938 . . . . . . . . . . . . 13
48 47 biimpar 485 . . . . . . . . . . . 12
49 r1sdom 8213 . . . . . . . . . . . 12
50 48 , 49 syldan 470 . . . . . . . . . . 11
51 46 , 50 syl5eqbrr 4486 . . . . . . . . . 10
52 fvex 5881 . . . . . . . . . . 11
53 52 0sdom 7668 . . . . . . . . . 10
54 51 , 53 sylib 196 . . . . . . . . 9
55 54 adantlr 714 . . . . . . . 8
56 tskcard 9180 . . . . . . . 8
57 2 , 55 , 56 syl2anc 661 . . . . . . 7
58 45 , 57 eqeltrrd 2546 . . . . . 6
59 58 ex 434 . . . . 5
60 1 , 59 syl5bir 218 . . . 4
61 60 orrd 378 . . 3
62 61 ex 434 . 2
63 fveq2 5871 . . . . 5
64 63 , 46 syl6eq 2514 . . . 4
65 0tsk 9154 . . . 4
66 64 , 65 syl6eqel 2553 . . 3
67 inatsk 9177 . . 3
68 66 , 67 jaoi 379 . 2
69 62 , 68 impbid1 203 1
