Step |
Hyp |
Ref |
Expression |
1 |
|
ordsson |
|
2 |
1
|
3ad2ant2 |
|
3 |
2
|
sseld |
|
4 |
|
eleq1w |
|
5 |
|
fveq2 |
|
6 |
|
id |
|
7 |
5 6
|
eqeq12d |
|
8 |
4 7
|
imbi12d |
|
9 |
8
|
imbi2d |
|
10 |
|
r19.21v |
|
11 |
|
ordelss |
|
12 |
11
|
3ad2antl2 |
|
13 |
12
|
sselda |
|
14 |
|
pm5.5 |
|
15 |
13 14
|
syl |
|
16 |
15
|
ralbidva |
|
17 |
|
isof1o |
|
18 |
17
|
3ad2ant1 |
|
19 |
18
|
ad2antrr |
|
20 |
|
simpll3 |
|
21 |
|
simpr |
|
22 |
|
f1of |
|
23 |
17 22
|
syl |
|
24 |
23
|
3ad2ant1 |
|
25 |
24
|
ad2antrr |
|
26 |
|
simplrl |
|
27 |
25 26
|
ffvelrnd |
|
28 |
21 27
|
jca |
|
29 |
|
ordtr1 |
|
30 |
20 28 29
|
sylc |
|
31 |
|
f1ocnvfv2 |
|
32 |
19 30 31
|
syl2anc |
|
33 |
32 21
|
eqeltrd |
|
34 |
|
simpll1 |
|
35 |
|
f1ocnv |
|
36 |
|
f1of |
|
37 |
19 35 36
|
3syl |
|
38 |
37 30
|
ffvelrnd |
|
39 |
|
isorel |
|
40 |
34 38 26 39
|
syl12anc |
|
41 |
|
epel |
|
42 |
|
fvex |
|
43 |
42
|
epeli |
|
44 |
40 41 43
|
3bitr3g |
|
45 |
33 44
|
mpbird |
|
46 |
|
simplrr |
|
47 |
|
fveq2 |
|
48 |
|
id |
|
49 |
47 48
|
eqeq12d |
|
50 |
49
|
rspcv |
|
51 |
45 46 50
|
sylc |
|
52 |
32 51
|
eqtr3d |
|
53 |
52 45
|
eqeltrd |
|
54 |
|
simprr |
|
55 |
|
fveq2 |
|
56 |
|
id |
|
57 |
55 56
|
eqeq12d |
|
58 |
57
|
rspccva |
|
59 |
54 58
|
sylan |
|
60 |
|
epel |
|
61 |
60
|
biimpri |
|
62 |
61
|
adantl |
|
63 |
|
simpll1 |
|
64 |
|
simpl2 |
|
65 |
|
simprl |
|
66 |
64 65 11
|
syl2anc |
|
67 |
66
|
sselda |
|
68 |
|
simplrl |
|
69 |
|
isorel |
|
70 |
63 67 68 69
|
syl12anc |
|
71 |
62 70
|
mpbid |
|
72 |
42
|
epeli |
|
73 |
71 72
|
sylib |
|
74 |
59 73
|
eqeltrrd |
|
75 |
53 74
|
impbida |
|
76 |
75
|
eqrdv |
|
77 |
76
|
expr |
|
78 |
16 77
|
sylbid |
|
79 |
78
|
ex |
|
80 |
79
|
com23 |
|
81 |
80
|
a2i |
|
82 |
81
|
a1i |
|
83 |
10 82
|
syl5bi |
|
84 |
9 83
|
tfis2 |
|
85 |
84
|
com3l |
|
86 |
3 85
|
mpdd |
|
87 |
86
|
ralrimiv |
|
88 |
|
fveq2 |
|
89 |
|
id |
|
90 |
88 89
|
eqeq12d |
|
91 |
90
|
rspccva |
|
92 |
91
|
adantll |
|
93 |
23
|
ffvelrnda |
|
94 |
93
|
3ad2antl1 |
|
95 |
94
|
adantlr |
|
96 |
92 95
|
eqeltrrd |
|
97 |
96
|
ex |
|
98 |
|
simpl1 |
|
99 |
|
f1ofo |
|
100 |
|
forn |
|
101 |
17 99 100
|
3syl |
|
102 |
98 101
|
syl |
|
103 |
102
|
eleq2d |
|
104 |
|
f1ofn |
|
105 |
17 104
|
syl |
|
106 |
105
|
3ad2ant1 |
|
107 |
106
|
adantr |
|
108 |
|
fvelrnb |
|
109 |
107 108
|
syl |
|
110 |
103 109
|
bitr3d |
|
111 |
|
fveq2 |
|
112 |
|
id |
|
113 |
111 112
|
eqeq12d |
|
114 |
113
|
rspcv |
|
115 |
114
|
a1i |
|
116 |
|
simpr |
|
117 |
|
simpl |
|
118 |
116 117
|
eqtr3d |
|
119 |
118
|
adantl |
|
120 |
|
simplr |
|
121 |
119 120
|
eqeltrd |
|
122 |
121
|
exp43 |
|
123 |
115 122
|
syldd |
|
124 |
123
|
com23 |
|
125 |
124
|
imp |
|
126 |
125
|
rexlimdv |
|
127 |
110 126
|
sylbid |
|
128 |
97 127
|
impbid |
|
129 |
128
|
eqrdv |
|
130 |
87 129
|
mpdan |
|