Step | Hyp | Ref
| Expression |
1 | | bren 6721 |
. . . . . 6
|
2 | 1 | biimpi 119 |
. . . . 5
|
3 | 2 | 3ad2ant1 1013 |
. . . 4
|
4 | 3 | adantr 274 |
. . 3
|
5 | | simplr 525 |
. . . . . . . . . . 11
|
6 | | simpr 109 |
. . . . . . . . . . 11
|
7 | 5, 6 | eqtr4d 2206 |
. . . . . . . . . 10
|
8 | | f1of1 5439 |
. . . . . . . . . . . . . 14
|
9 | 8 | adantl 275 |
. . . . . . . . . . . . 13
|
10 | 9 | adantr 274 |
. . . . . . . . . . . 12
|
11 | | simpr 109 |
. . . . . . . . . . . 12
|
12 | | simpll3 1033 |
. . . . . . . . . . . . 13
|
13 | 12 | adantr 274 |
. . . . . . . . . . . 12
|
14 | | f1fveq 5748 |
. . . . . . . . . . . 12
|
15 | 10, 11, 13, 14 | syl12anc 1231 |
. . . . . . . . . . 11
|
16 | 15 | ad2antrr 485 |
. . . . . . . . . 10
|
17 | 7, 16 | mpbid 146 |
. . . . . . . . 9
|
18 | | prid2g 3686 |
. . . . . . . . . . 11
|
19 | 13, 18 | syl 14 |
. . . . . . . . . 10
|
20 | 19 | ad2antrr 485 |
. . . . . . . . 9
|
21 | 17, 20 | eqeltrd 2247 |
. . . . . . . 8
|
22 | | simpllr 529 |
. . . . . . . . . . . 12
|
23 | | simpr 109 |
. . . . . . . . . . . 12
|
24 | 22, 23 | eqtr4d 2206 |
. . . . . . . . . . 11
|
25 | | simpll2 1032 |
. . . . . . . . . . . . . 14
|
26 | 25 | adantr 274 |
. . . . . . . . . . . . 13
|
27 | | f1fveq 5748 |
. . . . . . . . . . . . 13
|
28 | 10, 11, 26, 27 | syl12anc 1231 |
. . . . . . . . . . . 12
|
29 | 28 | ad3antrrr 489 |
. . . . . . . . . . 11
|
30 | 24, 29 | mpbid 146 |
. . . . . . . . . 10
|
31 | | prid1g 3685 |
. . . . . . . . . . . 12
|
32 | 26, 31 | syl 14 |
. . . . . . . . . . 11
|
33 | 32 | ad3antrrr 489 |
. . . . . . . . . 10
|
34 | 30, 33 | eqeltrd 2247 |
. . . . . . . . 9
|
35 | | simpr 109 |
. . . . . . . . . . 11
|
36 | | simplr 525 |
. . . . . . . . . . 11
|
37 | 35, 36 | eqtr4d 2206 |
. . . . . . . . . 10
|
38 | | simplr 525 |
. . . . . . . . . . . . 13
|
39 | 38 | neneqd 2361 |
. . . . . . . . . . . 12
|
40 | | f1fveq 5748 |
. . . . . . . . . . . . 13
|
41 | 9, 25, 12, 40 | syl12anc 1231 |
. . . . . . . . . . . 12
|
42 | 39, 41 | mtbird 668 |
. . . . . . . . . . 11
|
43 | 42 | ad4antr 491 |
. . . . . . . . . 10
|
44 | 37, 43 | pm2.21dd 615 |
. . . . . . . . 9
|
45 | | f1of 5440 |
. . . . . . . . . . . . 13
|
46 | 45 | adantl 275 |
. . . . . . . . . . . 12
|
47 | 46, 25 | ffvelrnd 5629 |
. . . . . . . . . . 11
|
48 | | elpri 3604 |
. . . . . . . . . . . 12
|
49 | | df2o3 6406 |
. . . . . . . . . . . 12
|
50 | 48, 49 | eleq2s 2265 |
. . . . . . . . . . 11
|
51 | 47, 50 | syl 14 |
. . . . . . . . . 10
|
52 | 51 | ad3antrrr 489 |
. . . . . . . . 9
|
53 | 34, 44, 52 | mpjaodan 793 |
. . . . . . . 8
|
54 | 46, 12 | ffvelrnd 5629 |
. . . . . . . . . 10
|
55 | | elpri 3604 |
. . . . . . . . . . 11
|
56 | 55, 49 | eleq2s 2265 |
. . . . . . . . . 10
|
57 | 54, 56 | syl 14 |
. . . . . . . . 9
|
58 | 57 | ad2antrr 485 |
. . . . . . . 8
|
59 | 21, 53, 58 | mpjaodan 793 |
. . . . . . 7
|
60 | | simpr 109 |
. . . . . . . . . . 11
|
61 | | simplr 525 |
. . . . . . . . . . 11
|
62 | 60, 61 | eqtr4d 2206 |
. . . . . . . . . 10
|
63 | 42 | ad4antr 491 |
. . . . . . . . . 10
|
64 | 62, 63 | pm2.21dd 615 |
. . . . . . . . 9
|
65 | | simpllr 529 |
. . . . . . . . . . . 12
|
66 | | simpr 109 |
. . . . . . . . . . . 12
|
67 | 65, 66 | eqtr4d 2206 |
. . . . . . . . . . 11
|
68 | 28 | ad3antrrr 489 |
. . . . . . . . . . 11
|
69 | 67, 68 | mpbid 146 |
. . . . . . . . . 10
|
70 | 32 | ad3antrrr 489 |
. . . . . . . . . 10
|
71 | 69, 70 | eqeltrd 2247 |
. . . . . . . . 9
|
72 | 51 | ad3antrrr 489 |
. . . . . . . . 9
|
73 | 64, 71, 72 | mpjaodan 793 |
. . . . . . . 8
|
74 | | simplr 525 |
. . . . . . . . . . 11
|
75 | | simpr 109 |
. . . . . . . . . . 11
|
76 | 74, 75 | eqtr4d 2206 |
. . . . . . . . . 10
|
77 | 15 | ad2antrr 485 |
. . . . . . . . . 10
|
78 | 76, 77 | mpbid 146 |
. . . . . . . . 9
|
79 | 19 | ad2antrr 485 |
. . . . . . . . 9
|
80 | 78, 79 | eqeltrd 2247 |
. . . . . . . 8
|
81 | 57 | ad2antrr 485 |
. . . . . . . 8
|
82 | 73, 80, 81 | mpjaodan 793 |
. . . . . . 7
|
83 | 46 | ffvelrnda 5628 |
. . . . . . . 8
|
84 | | elpri 3604 |
. . . . . . . . 9
|
85 | 84, 49 | eleq2s 2265 |
. . . . . . . 8
|
86 | 83, 85 | syl 14 |
. . . . . . 7
|
87 | 59, 82, 86 | mpjaodan 793 |
. . . . . 6
|
88 | 87 | ex 114 |
. . . . 5
|
89 | 88 | ssrdv 3153 |
. . . 4
|
90 | | prssi 3736 |
. . . . 5
|
91 | 25, 12, 90 | syl2anc 409 |
. . . 4
|
92 | 89, 91 | eqssd 3164 |
. . 3
|
93 | 4, 92 | exlimddv 1891 |
. 2
|
94 | 93 | ex 114 |
1
|