Step | Hyp | Ref
| Expression |
1 | | n0 3931 |
. . . 4
|
2 | | 0ss 3972 |
. . . . . . . . . 10
|
3 | | gruss 9618 |
. . . . . . . . . 10
|
4 | 2, 3 | mp3an3 1413 |
. . . . . . . . 9
|
5 | | 0elon 5778 |
. . . . . . . . 9
|
6 | | elin 3796 |
. . . . . . . . 9
|
7 | 4, 5, 6 | sylanblrc 697 |
. . . . . . . 8
|
8 | | gruina.1 |
. . . . . . . 8
|
9 | 7, 8 | syl6eleqr 2712 |
. . . . . . 7
|
10 | | ne0i 3921 |
. . . . . . 7
|
11 | 9, 10 | syl 17 |
. . . . . 6
|
12 | 11 | expcom 451 |
. . . . 5
|
13 | 12 | exlimiv 1858 |
. . . 4
|
14 | 1, 13 | sylbi 207 |
. . 3
|
15 | 14 | impcom 446 |
. 2
|
16 | | grutr 9615 |
. . . . . . . 8
|
17 | | tron 5746 |
. . . . . . . 8
|
18 | | trin 4763 |
. . . . . . . 8
|
19 | 16, 17, 18 | sylancl 694 |
. . . . . . 7
|
20 | | inss2 3834 |
. . . . . . . 8
|
21 | | epweon 6983 |
. . . . . . . 8
|
22 | | wess 5101 |
. . . . . . . 8
|
23 | 20, 21, 22 | mp2 9 |
. . . . . . 7
|
24 | | df-ord 5726 |
. . . . . . 7
|
25 | 19, 23, 24 | sylanblrc 697 |
. . . . . 6
|
26 | | inex1g 4801 |
. . . . . 6
|
27 | | elon2 5734 |
. . . . . 6
|
28 | 25, 26, 27 | sylanbrc 698 |
. . . . 5
|
29 | 8, 28 | syl5eqel 2705 |
. . . 4
|
30 | 29 | adantr 481 |
. . 3
|
31 | | eloni 5733 |
. . . . . . 7
|
32 | | ordirr 5741 |
. . . . . . 7
|
33 | 31, 32 | syl 17 |
. . . . . 6
|
34 | | elin 3796 |
. . . . . . . . 9
|
35 | 34 | biimpri 218 |
. . . . . . . 8
|
36 | 35, 8 | syl6eleqr 2712 |
. . . . . . 7
|
37 | 36 | expcom 451 |
. . . . . 6
|
38 | 33, 37 | mtod 189 |
. . . . 5
|
39 | 30, 38 | syl 17 |
. . . 4
|
40 | | inss1 3833 |
. . . . . . . . . . . . . . . 16
|
41 | 8, 40 | eqsstri 3635 |
. . . . . . . . . . . . . . 15
|
42 | 41 | sseli 3599 |
. . . . . . . . . . . . . 14
|
43 | | vpwex 4849 |
. . . . . . . . . . . . . . . 16
|
44 | 43 | canth2 8113 |
. . . . . . . . . . . . . . 15
|
45 | 43 | pwex 4848 |
. . . . . . . . . . . . . . . . . 18
|
46 | 45 | cardid 9369 |
. . . . . . . . . . . . . . . . 17
|
47 | 46 | ensymi 8006 |
. . . . . . . . . . . . . . . 16
|
48 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
49 | | grupw 9617 |
. . . . . . . . . . . . . . . . . . 19
|
50 | | grupw 9617 |
. . . . . . . . . . . . . . . . . . 19
|
51 | 49, 50 | syldan 487 |
. . . . . . . . . . . . . . . . . 18
|
52 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
53 | | endom 7982 |
. . . . . . . . . . . . . . . . . . . . . 22
|
54 | 46, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
|
55 | | cardon 8770 |
. . . . . . . . . . . . . . . . . . . . . 22
|
56 | | grudomon 9639 |
. . . . . . . . . . . . . . . . . . . . . 22
|
57 | 55, 56 | mp3an2 1412 |
. . . . . . . . . . . . . . . . . . . . 21
|
58 | 54, 57 | mpanr2 720 |
. . . . . . . . . . . . . . . . . . . 20
|
59 | | elin 3796 |
. . . . . . . . . . . . . . . . . . . . . 22
|
60 | 59 | biimpri 218 |
. . . . . . . . . . . . . . . . . . . . 21
|
61 | 60, 8 | syl6eleqr 2712 |
. . . . . . . . . . . . . . . . . . . 20
|
62 | 58, 55, 61 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
|
63 | | onelss 5766 |
. . . . . . . . . . . . . . . . . . 19
|
64 | 52, 62, 63 | sylc 65 |
. . . . . . . . . . . . . . . . . 18
|
65 | 51, 64 | syldan 487 |
. . . . . . . . . . . . . . . . 17
|
66 | | ssdomg 8001 |
. . . . . . . . . . . . . . . . 17
|
67 | 48, 65, 66 | sylc 65 |
. . . . . . . . . . . . . . . 16
|
68 | | endomtr 8014 |
. . . . . . . . . . . . . . . 16
|
69 | 47, 67, 68 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
70 | | sdomdomtr 8093 |
. . . . . . . . . . . . . . 15
|
71 | 44, 69, 70 | sylancr 695 |
. . . . . . . . . . . . . 14
|
72 | 42, 71 | sylan2 491 |
. . . . . . . . . . . . 13
|
73 | 72 | ralrimiva 2966 |
. . . . . . . . . . . 12
|
74 | | inawinalem 9511 |
. . . . . . . . . . . 12
|
75 | 29, 73, 74 | sylc 65 |
. . . . . . . . . . 11
|
76 | 75 | adantr 481 |
. . . . . . . . . 10
|
77 | | winainflem 9515 |
. . . . . . . . . 10
|
78 | 15, 30, 76, 77 | syl3anc 1326 |
. . . . . . . . 9
|
79 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
80 | 79 | canth2 8113 |
. . . . . . . . . . . . . 14
|
81 | | sdomtr 8098 |
. . . . . . . . . . . . . 14
|
82 | 80, 72, 81 | sylancr 695 |
. . . . . . . . . . . . 13
|
83 | 82 | ralrimiva 2966 |
. . . . . . . . . . . 12
|
84 | | iscard 8801 |
. . . . . . . . . . . 12
|
85 | 29, 83, 84 | sylanbrc 698 |
. . . . . . . . . . 11
|
86 | | cardlim 8798 |
. . . . . . . . . . . 12
|
87 | | sseq2 3627 |
. . . . . . . . . . . . 13
|
88 | | limeq 5735 |
. . . . . . . . . . . . 13
|
89 | 87, 88 | bibi12d 335 |
. . . . . . . . . . . 12
|
90 | 86, 89 | mpbii 223 |
. . . . . . . . . . 11
|
91 | 85, 90 | syl 17 |
. . . . . . . . . 10
|
92 | 91 | adantr 481 |
. . . . . . . . 9
|
93 | 78, 92 | mpbid 222 |
. . . . . . . 8
|
94 | | cflm 9072 |
. . . . . . . 8
|
95 | 30, 93, 94 | syl2anc 693 |
. . . . . . 7
|
96 | | cardon 8770 |
. . . . . . . . . . . 12
|
97 | | eleq1 2689 |
. . . . . . . . . . . 12
|
98 | 96, 97 | mpbiri 248 |
. . . . . . . . . . 11
|
99 | 98 | adantr 481 |
. . . . . . . . . 10
|
100 | 99 | exlimiv 1858 |
. . . . . . . . 9
|
101 | 100 | abssi 3677 |
. . . . . . . 8
|
102 | | fvex 6201 |
. . . . . . . . . 10
|
103 | 95, 102 | syl6eqelr 2710 |
. . . . . . . . 9
|
104 | | intex 4820 |
. . . . . . . . 9
|
105 | 103, 104 | sylibr 224 |
. . . . . . . 8
|
106 | | onint 6995 |
. . . . . . . 8
|
107 | 101, 105,
106 | sylancr 695 |
. . . . . . 7
|
108 | 95, 107 | eqeltrd 2701 |
. . . . . 6
|
109 | | eqeq1 2626 |
. . . . . . . . 9
|
110 | 109 | anbi1d 741 |
. . . . . . . 8
|
111 | 110 | exbidv 1850 |
. . . . . . 7
|
112 | 102, 111 | elab 3350 |
. . . . . 6
|
113 | 108, 112 | sylib 208 |
. . . . 5
|
114 | | simp2rr 1131 |
. . . . . . . 8
|
115 | | simp1l 1085 |
. . . . . . . . 9
|
116 | | simp2rl 1130 |
. . . . . . . . . . 11
|
117 | 116, 41 | syl6ss 3615 |
. . . . . . . . . 10
|
118 | 41 | sseli 3599 |
. . . . . . . . . . 11
|
119 | 118 | 3ad2ant3 1084 |
. . . . . . . . . 10
|
120 | | simp2l 1087 |
. . . . . . . . . . 11
|
121 | | vex 3203 |
. . . . . . . . . . . 12
|
122 | 121 | cardid 9369 |
. . . . . . . . . . 11
|
123 | 120, 122 | syl6eqbr 4692 |
. . . . . . . . . 10
|
124 | | gruen 9634 |
. . . . . . . . . 10
|
125 | 115, 117,
119, 123, 124 | syl112anc 1330 |
. . . . . . . . 9
|
126 | | gruuni 9622 |
. . . . . . . . 9
|
127 | 115, 125,
126 | syl2anc 693 |
. . . . . . . 8
|
128 | 114, 127 | eqeltrd 2701 |
. . . . . . 7
|
129 | 128 | 3exp 1264 |
. . . . . 6
|
130 | 129 | exlimdv 1861 |
. . . . 5
|
131 | 113, 130 | mpd 15 |
. . . 4
|
132 | 39, 131 | mtod 189 |
. . 3
|
133 | | cfon 9077 |
. . . . 5
|
134 | | cfle 9076 |
. . . . . 6
|
135 | | onsseleq 5765 |
. . . . . 6
|
136 | 134, 135 | mpbii 223 |
. . . . 5
|
137 | 133, 136 | mpan 706 |
. . . 4
|
138 | 137 | ord 392 |
. . 3
|
139 | 30, 132, 138 | sylc 65 |
. 2
|
140 | 73 | adantr 481 |
. 2
|
141 | | elina 9509 |
. 2
|
142 | 15, 139, 140, 141 | syl3anbrc 1246 |
1
|