Step | Hyp | Ref
| Expression |
1 | | heibor.1 |
. . 3
|
2 | 1 | heibor1 33609 |
. 2
|
3 | | cmetmet 23084 |
. . . 4
|
4 | 3 | adantr 481 |
. . 3
|
5 | | metxmet 22139 |
. . . . . 6
|
6 | 1 | mopntop 22245 |
. . . . . 6
|
7 | 3, 5, 6 | 3syl 18 |
. . . . 5
|
8 | 7 | adantr 481 |
. . . 4
|
9 | | istotbnd 33568 |
. . . . . . . . . . . . 13
|
10 | 9 | simprbi 480 |
. . . . . . . . . . . 12
|
11 | | 2nn 11185 |
. . . . . . . . . . . . . . 15
|
12 | | nnexpcl 12873 |
. . . . . . . . . . . . . . 15
|
13 | 11, 12 | mpan 706 |
. . . . . . . . . . . . . 14
|
14 | 13 | nnrpd 11870 |
. . . . . . . . . . . . 13
|
15 | 14 | rpreccld 11882 |
. . . . . . . . . . . 12
|
16 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . 18
|
17 | 16 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . 17
|
18 | 17 | rexbidv 3052 |
. . . . . . . . . . . . . . . 16
|
19 | 18 | ralbidv 2986 |
. . . . . . . . . . . . . . 15
|
20 | 19 | anbi2d 740 |
. . . . . . . . . . . . . 14
|
21 | 20 | rexbidv 3052 |
. . . . . . . . . . . . 13
|
22 | 21 | rspccva 3308 |
. . . . . . . . . . . 12
|
23 | 10, 15, 22 | syl2an 494 |
. . . . . . . . . . 11
|
24 | 23 | expcom 451 |
. . . . . . . . . 10
|
25 | 24 | adantl 482 |
. . . . . . . . 9
|
26 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
|
27 | 26 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
|
28 | 27 | ac6sfi 8204 |
. . . . . . . . . . . . 13
|
29 | 28 | adantrl 752 |
. . . . . . . . . . . 12
|
30 | 29 | adantl 482 |
. . . . . . . . . . 11
|
31 | | simp3l 1089 |
. . . . . . . . . . . . . . . . . . 19
|
32 | | frn 6053 |
. . . . . . . . . . . . . . . . . . 19
|
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
34 | 1 | mopnuni 22246 |
. . . . . . . . . . . . . . . . . . . . 21
|
35 | 3, 5, 34 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
|
36 | 35 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
37 | 36 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . 18
|
38 | 33, 37 | sseqtrd 3641 |
. . . . . . . . . . . . . . . . 17
|
39 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . 20
|
40 | 1, 39 | eqeltri 2697 |
. . . . . . . . . . . . . . . . . . 19
|
41 | 40 | uniex 6953 |
. . . . . . . . . . . . . . . . . 18
|
42 | 41 | elpw2 4828 |
. . . . . . . . . . . . . . . . 17
|
43 | 38, 42 | sylibr 224 |
. . . . . . . . . . . . . . . 16
|
44 | | simp2l 1087 |
. . . . . . . . . . . . . . . . 17
|
45 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . 19
|
46 | | dffn4 6121 |
. . . . . . . . . . . . . . . . . . 19
|
47 | 45, 46 | sylib 208 |
. . . . . . . . . . . . . . . . . 18
|
48 | | fofi 8252 |
. . . . . . . . . . . . . . . . . 18
|
49 | 47, 48 | sylan2 491 |
. . . . . . . . . . . . . . . . 17
|
50 | 44, 31, 49 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
51 | 43, 50 | elind 3798 |
. . . . . . . . . . . . . . 15
|
52 | 26 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . 20
|
53 | 52 | rexrn 6361 |
. . . . . . . . . . . . . . . . . . 19
|
54 | | eliun 4524 |
. . . . . . . . . . . . . . . . . . 19
|
55 | | eliun 4524 |
. . . . . . . . . . . . . . . . . . 19
|
56 | 53, 54, 55 | 3bitr4g 303 |
. . . . . . . . . . . . . . . . . 18
|
57 | 56 | eqrdv 2620 |
. . . . . . . . . . . . . . . . 17
|
58 | 31, 45, 57 | 3syl 18 |
. . . . . . . . . . . . . . . 16
|
59 | | simp3r 1090 |
. . . . . . . . . . . . . . . . 17
|
60 | | uniiun 4573 |
. . . . . . . . . . . . . . . . . 18
|
61 | | iuneq2 4537 |
. . . . . . . . . . . . . . . . . 18
|
62 | 60, 61 | syl5eq 2668 |
. . . . . . . . . . . . . . . . 17
|
63 | 59, 62 | syl 17 |
. . . . . . . . . . . . . . . 16
|
64 | | simp2r 1088 |
. . . . . . . . . . . . . . . 16
|
65 | 58, 63, 64 | 3eqtr2rd 2663 |
. . . . . . . . . . . . . . 15
|
66 | | iuneq1 4534 |
. . . . . . . . . . . . . . . . 17
|
67 | 66 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
|
68 | 67 | rspcev 3309 |
. . . . . . . . . . . . . . 15
|
69 | 51, 65, 68 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
70 | 69 | 3expia 1267 |
. . . . . . . . . . . . 13
|
71 | 70 | adantrrr 761 |
. . . . . . . . . . . 12
|
72 | 71 | exlimdv 1861 |
. . . . . . . . . . 11
|
73 | 30, 72 | mpd 15 |
. . . . . . . . . 10
|
74 | 73 | rexlimdvaa 3032 |
. . . . . . . . 9
|
75 | 25, 74 | syld 47 |
. . . . . . . 8
|
76 | 75 | ralrimdva 2969 |
. . . . . . 7
|
77 | 41 | pwex 4848 |
. . . . . . . . 9
|
78 | 77 | inex1 4799 |
. . . . . . . 8
|
79 | | nn0ennn 12778 |
. . . . . . . . 9
|
80 | | nnenom 12779 |
. . . . . . . . 9
|
81 | 79, 80 | entri 8010 |
. . . . . . . 8
|
82 | | iuneq1 4534 |
. . . . . . . . 9
|
83 | 82 | eqeq2d 2632 |
. . . . . . . 8
|
84 | 78, 81, 83 | axcc4 9261 |
. . . . . . 7
|
85 | 76, 84 | syl6 35 |
. . . . . 6
|
86 | | elpwi 4168 |
. . . . . . . . . 10
|
87 | | eqid 2622 |
. . . . . . . . . . . 12
|
88 | | eqid 2622 |
. . . . . . . . . . . 12
|
89 | | eqid 2622 |
. . . . . . . . . . . 12
|
90 | | simpl 473 |
. . . . . . . . . . . 12
|
91 | 35 | pweqd 4163 |
. . . . . . . . . . . . . . . 16
|
92 | 91 | ineq1d 3813 |
. . . . . . . . . . . . . . 15
|
93 | 92 | feq3d 6032 |
. . . . . . . . . . . . . 14
|
94 | 93 | biimpar 502 |
. . . . . . . . . . . . 13
|
95 | 94 | adantrr 753 |
. . . . . . . . . . . 12
|
96 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
|
97 | 96 | cbviunv 4559 |
. . . . . . . . . . . . . . . . . 18
|
98 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
99 | | inss1 3833 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
100 | 99, 91 | syl5sseqr 3654 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
101 | | fss 6056 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
102 | 98, 100, 101 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
103 | 102 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . 22
|
104 | 103 | elpwid 4170 |
. . . . . . . . . . . . . . . . . . . . 21
|
105 | 104 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . 20
|
106 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . 20
|
107 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . 21
|
108 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
109 | 108 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . 22
|
110 | 109 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . 21
|
111 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . 21
|
112 | 107, 110,
89, 111 | ovmpt2 6796 |
. . . . . . . . . . . . . . . . . . . 20
|
113 | 105, 106,
112 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
114 | 113 | iuneq2dv 4542 |
. . . . . . . . . . . . . . . . . 18
|
115 | 97, 114 | syl5eq 2668 |
. . . . . . . . . . . . . . . . 17
|
116 | 115 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
|
117 | 116 | biimprd 238 |
. . . . . . . . . . . . . . 15
|
118 | 117 | ralimdva 2962 |
. . . . . . . . . . . . . 14
|
119 | 118 | impr 649 |
. . . . . . . . . . . . 13
|
120 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
121 | 120 | iuneq1d 4545 |
. . . . . . . . . . . . . . . 16
|
122 | | simpl 473 |
. . . . . . . . . . . . . . . . . 18
|
123 | 122 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
124 | 123 | iuneq2dv 4542 |
. . . . . . . . . . . . . . . 16
|
125 | 121, 124 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
126 | 125 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
|
127 | 126 | cbvralv 3171 |
. . . . . . . . . . . . 13
|
128 | 119, 127 | sylib 208 |
. . . . . . . . . . . 12
|
129 | 1, 87, 88, 89, 90, 95, 128 | heiborlem10 33619 |
. . . . . . . . . . 11
|
130 | 129 | exp32 631 |
. . . . . . . . . 10
|
131 | 86, 130 | syl5 34 |
. . . . . . . . 9
|
132 | 131 | ralrimiv 2965 |
. . . . . . . 8
|
133 | 132 | ex 450 |
. . . . . . 7
|
134 | 133 | exlimdv 1861 |
. . . . . 6
|
135 | 85, 134 | syld 47 |
. . . . 5
|
136 | 135 | imp 445 |
. . . 4
|
137 | | eqid 2622 |
. . . . 5
|
138 | 137 | iscmp 21191 |
. . . 4
|
139 | 8, 136, 138 | sylanbrc 698 |
. . 3
|
140 | 4, 139 | jca 554 |
. 2
|
141 | 2, 140 | impbii 199 |
1
|