Step | Hyp | Ref
| Expression |
1 | | is2ndc 21249 |
. . 3
|
2 | | omex 8540 |
. . . . . . 7
|
3 | 2 | brdom 7967 |
. . . . . 6
|
4 | | ssrab2 3687 |
. . . . . . . . . . . . . . . . . . . 20
|
5 | | f1f 6101 |
. . . . . . . . . . . . . . . . . . . . . 22
|
6 | | frn 6053 |
. . . . . . . . . . . . . . . . . . . . . 22
|
7 | 5, 6 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
8 | 7 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
9 | 4, 8 | syl5ss 3614 |
. . . . . . . . . . . . . . . . . . 19
|
10 | 9 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
11 | | eldifsn 4317 |
. . . . . . . . . . . . . . . . . . . 20
|
12 | | n0 3931 |
. . . . . . . . . . . . . . . . . . . . . 22
|
13 | | tg2 20769 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
14 | | omsson 7069 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
15 | 9, 14 | syl6ss 3615 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
16 | 15 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
17 | | f1fn 6102 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
18 | 17 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
19 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
20 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
21 | 18, 19, 20 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
22 | | f1f1orn 6148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
23 | 22 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
24 | | f1ocnvfv1 6532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
25 | 23, 19, 24 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
26 | | simprrr 805 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
27 | | selpw 4165 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
28 | 26, 27 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
29 | | simprrl 804 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
30 | | ne0i 3921 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
32 | | eldifsn 4317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
33 | 28, 31, 32 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
34 | 25, 33 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
35 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
36 | 35 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
37 | 36 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
38 | 21, 34, 37 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
39 | | rabn0 3958 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
40 | 38, 39 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
41 | | onint 6995 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
42 | 16, 40, 41 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
43 | 42 | rexlimdvaa 3032 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
44 | 13, 43 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
45 | 44 | expdimp 453 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
46 | 45 | exlimdv 1861 |
. . . . . . . . . . . . . . . . . . . . . 22
|
47 | 12, 46 | syl5bi 232 |
. . . . . . . . . . . . . . . . . . . . 21
|
48 | 47 | expimpd 629 |
. . . . . . . . . . . . . . . . . . . 20
|
49 | 11, 48 | syl5bi 232 |
. . . . . . . . . . . . . . . . . . 19
|
50 | 49 | impr 649 |
. . . . . . . . . . . . . . . . . 18
|
51 | 10, 50 | sseldd 3604 |
. . . . . . . . . . . . . . . . 17
|
52 | 51 | expr 643 |
. . . . . . . . . . . . . . . 16
|
53 | 52 | ralimdva 2962 |
. . . . . . . . . . . . . . 15
|
54 | 53 | imp 445 |
. . . . . . . . . . . . . 14
|
55 | 54 | adantrr 753 |
. . . . . . . . . . . . 13
|
56 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
57 | 56 | fmpt 6381 |
. . . . . . . . . . . . 13
|
58 | 55, 57 | sylib 208 |
. . . . . . . . . . . 12
|
59 | | neeq1 2856 |
. . . . . . . . . . . . . . . . . . 19
|
60 | | neeq1 2856 |
. . . . . . . . . . . . . . . . . . 19
|
61 | | 1n0 7575 |
. . . . . . . . . . . . . . . . . . 19
|
62 | 59, 60, 61 | elimhyp 4146 |
. . . . . . . . . . . . . . . . . 18
|
63 | | n0 3931 |
. . . . . . . . . . . . . . . . . 18
|
64 | 62, 63 | mpbi 220 |
. . . . . . . . . . . . . . . . 17
|
65 | | 19.29r 1802 |
. . . . . . . . . . . . . . . . 17
|
66 | 64, 65 | mpan 706 |
. . . . . . . . . . . . . . . 16
|
67 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
68 | 50, 67 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
69 | 68 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
70 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
71 | 70 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
72 | 71 | elrab 3363 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
73 | 72 | simprbi 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
74 | 69, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
75 | | eldifsn 4317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
76 | 74, 75 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
77 | 76 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
78 | 77 | iftrued 4094 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
79 | 76 | simpld 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
80 | 79 | elpwid 4170 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
81 | 78, 80 | eqsstrd 3639 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
82 | 81 | sseld 3602 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
83 | 82 | exp31 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
84 | 83 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
85 | 84 | exp4a 633 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
86 | 85 | com25 99 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
87 | 86 | imp31 448 |
. . . . . . . . . . . . . . . . . . . . . 22
|
88 | 87 | ralimdva 2962 |
. . . . . . . . . . . . . . . . . . . . 21
|
89 | 88 | imp 445 |
. . . . . . . . . . . . . . . . . . . 20
|
90 | 89 | an32s 846 |
. . . . . . . . . . . . . . . . . . 19
|
91 | | rmoim 3407 |
. . . . . . . . . . . . . . . . . . 19
|
92 | 90, 91 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
93 | 92 | expimpd 629 |
. . . . . . . . . . . . . . . . 17
|
94 | 93 | exlimdv 1861 |
. . . . . . . . . . . . . . . 16
|
95 | 66, 94 | syl5 34 |
. . . . . . . . . . . . . . 15
|
96 | 95 | impr 649 |
. . . . . . . . . . . . . 14
|
97 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
|
98 | | nfmpt1 4747 |
. . . . . . . . . . . . . . . . 17
|
99 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
|
100 | 97, 98, 99 | nfbr 4699 |
. . . . . . . . . . . . . . . 16
|
101 | | nfv 1843 |
. . . . . . . . . . . . . . . 16
|
102 | | breq1 4656 |
. . . . . . . . . . . . . . . . 17
|
103 | | df-br 4654 |
. . . . . . . . . . . . . . . . . 18
|
104 | | df-mpt 4730 |
. . . . . . . . . . . . . . . . . . 19
|
105 | 104 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . 18
|
106 | | opabid 4982 |
. . . . . . . . . . . . . . . . . 18
|
107 | 103, 105,
106 | 3bitri 286 |
. . . . . . . . . . . . . . . . 17
|
108 | 102, 107 | syl6bb 276 |
. . . . . . . . . . . . . . . 16
|
109 | 100, 101,
108 | cbvmo 2506 |
. . . . . . . . . . . . . . 15
|
110 | | df-rmo 2920 |
. . . . . . . . . . . . . . 15
|
111 | 109, 110 | bitr4i 267 |
. . . . . . . . . . . . . 14
|
112 | 96, 111 | sylibr 224 |
. . . . . . . . . . . . 13
|
113 | 112 | alrimiv 1855 |
. . . . . . . . . . . 12
|
114 | | dff12 6100 |
. . . . . . . . . . . 12
|
115 | 58, 113, 114 | sylanbrc 698 |
. . . . . . . . . . 11
|
116 | | f1domg 7975 |
. . . . . . . . . . 11
|
117 | 2, 115, 116 | mpsyl 68 |
. . . . . . . . . 10
|
118 | 117 | ex 450 |
. . . . . . . . 9
|
119 | | difeq1 3721 |
. . . . . . . . . . . . 13
|
120 | 119 | eleq2d 2687 |
. . . . . . . . . . . 12
|
121 | 120 | ralbidv 2986 |
. . . . . . . . . . 11
|
122 | 121 | anbi1d 741 |
. . . . . . . . . 10
|
123 | 122 | imbi1d 331 |
. . . . . . . . 9
|
124 | 118, 123 | syl5ibcom 235 |
. . . . . . . 8
|
125 | 124 | ex 450 |
. . . . . . 7
|
126 | 125 | exlimdv 1861 |
. . . . . 6
|
127 | 3, 126 | syl5bi 232 |
. . . . 5
|
128 | 127 | impd 447 |
. . . 4
|
129 | 128 | rexlimiv 3027 |
. . 3
|
130 | 1, 129 | sylbi 207 |
. 2
|
131 | 130 | 3impib 1262 |
1
|