Step | Hyp | Ref
| Expression |
1 | | 2z 11409 |
. . . 4
|
2 | | uzid 11702 |
. . . 4
|
3 | 1, 2 | ax-mp 5 |
. . 3
|
4 | | istrkg.p |
. . . 4
|
5 | | istrkg.d |
. . . 4
|
6 | | istrkg.i |
. . . 4
Itv |
7 | 4, 5, 6 | istrkgld 25358 |
. . 3
DimTarskiG≥ ..^
..^
|
8 | 3, 7 | mpan2 707 |
. 2
DimTarskiG≥ ..^
..^
|
9 | | r19.41v 3089 |
. . . . 5
..^ ..^
..^ ..^ |
10 | | ancom 466 |
. . . . . 6
..^ ..^
..^
..^
|
11 | 10 | rexbii 3041 |
. . . . 5
..^ ..^
..^
..^
|
12 | | ancom 466 |
. . . . 5
..^ ..^
..^
..^
|
13 | 9, 11, 12 | 3bitr3ri 291 |
. . . 4
..^
..^
..^
..^ |
14 | 13 | exbii 1774 |
. . 3
..^
..^
..^
..^ |
15 | | rexcom4 3225 |
. . 3
..^
..^
..^
..^ |
16 | | simpr 477 |
. . . . . . . . . 10
..^ |
17 | 16 | reximi 3011 |
. . . . . . . . 9
..^
|
18 | 17 | reximi 3011 |
. . . . . . . 8
..^
|
19 | 18 | adantl 482 |
. . . . . . 7
..^
..^
|
20 | 19 | exlimiv 1858 |
. . . . . 6
..^
..^
|
21 | 20 | adantl 482 |
. . . . 5
..^
..^
|
22 | | 1ex 10035 |
. . . . . . . . . 10
|
23 | | vex 3203 |
. . . . . . . . . 10
|
24 | 22, 23 | f1osn 6176 |
. . . . . . . . 9
|
25 | | f1of1 6136 |
. . . . . . . . 9
|
26 | 24, 25 | mp1i 13 |
. . . . . . . 8
|
27 | | snssi 4339 |
. . . . . . . 8
|
28 | | f1ss 6106 |
. . . . . . . 8
|
29 | 26, 27, 28 | syl2anc 693 |
. . . . . . 7
|
30 | | fzo12sn 12551 |
. . . . . . . . . . . 12
..^ |
31 | | mpteq1 4737 |
. . . . . . . . . . . 12
..^ ..^ |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . . 11
..^ |
33 | | fmptsn 6433 |
. . . . . . . . . . . 12
|
34 | 22, 23, 33 | mp2an 708 |
. . . . . . . . . . 11
|
35 | 32, 34 | eqtr4i 2647 |
. . . . . . . . . 10
..^ |
36 | 35 | a1i 11 |
. . . . . . . . 9
..^
|
37 | 30 | a1i 11 |
. . . . . . . . 9
..^ |
38 | | eqidd 2623 |
. . . . . . . . 9
|
39 | 36, 37, 38 | f1eq123d 6131 |
. . . . . . . 8
..^ ..^ |
40 | 39 | trud 1493 |
. . . . . . 7
..^ ..^
|
41 | 29, 40 | sylibr 224 |
. . . . . 6
..^ ..^ |
42 | | ral0 4076 |
. . . . . . . . . 10
..^ ..^
..^ ..^
..^ ..^ |
43 | | fzo0 12492 |
. . . . . . . . . . 11
..^ |
44 | 43 | raleqi 3142 |
. . . . . . . . . 10
..^ ..^
..^ ..^
..^ ..^
..^
..^ ..^
..^ ..^
..^ ..^ |
45 | 42, 44 | mpbir 221 |
. . . . . . . . 9
..^ ..^ ..^
..^ ..^ ..^ ..^ |
46 | 45 | jctl 564 |
. . . . . . . 8
..^ ..^
..^ ..^
..^ ..^
..^ |
47 | 46 | reximi 3011 |
. . . . . . 7
..^ ..^
..^ ..^
..^ ..^
..^ |
48 | 47 | reximi 3011 |
. . . . . 6
..^ ..^
..^ ..^
..^ ..^
..^ |
49 | | ovex 6678 |
. . . . . . . 8
..^ |
50 | 49 | mptex 6486 |
. . . . . . 7
..^ |
51 | | f1eq1 6096 |
. . . . . . . 8
..^ ..^
..^ ..^ |
52 | | nfmpt1 4747 |
. . . . . . . . . . . . 13
..^ |
53 | 52 | nfeq2 2780 |
. . . . . . . . . . . 12
..^ |
54 | | nfv 1843 |
. . . . . . . . . . . 12
|
55 | 53, 54 | nfan 1828 |
. . . . . . . . . . 11
..^ |
56 | | simpll 790 |
. . . . . . . . . . . . . . 15
..^
..^ ..^ |
57 | 56 | fveq1d 6193 |
. . . . . . . . . . . . . 14
..^
..^ ..^ |
58 | 57 | oveq1d 6665 |
. . . . . . . . . . . . 13
..^
..^ ..^ |
59 | 56 | fveq1d 6193 |
. . . . . . . . . . . . . 14
..^
..^ ..^ |
60 | 59 | oveq1d 6665 |
. . . . . . . . . . . . 13
..^
..^ ..^ |
61 | 58, 60 | eqeq12d 2637 |
. . . . . . . . . . . 12
..^
..^
..^
..^ |
62 | 57 | oveq1d 6665 |
. . . . . . . . . . . . 13
..^
..^ ..^ |
63 | 59 | oveq1d 6665 |
. . . . . . . . . . . . 13
..^
..^ ..^ |
64 | 62, 63 | eqeq12d 2637 |
. . . . . . . . . . . 12
..^
..^
..^
..^ |
65 | 57 | oveq1d 6665 |
. . . . . . . . . . . . 13
..^
..^ ..^ |
66 | 59 | oveq1d 6665 |
. . . . . . . . . . . . 13
..^
..^ ..^ |
67 | 65, 66 | eqeq12d 2637 |
. . . . . . . . . . . 12
..^
..^
..^
..^ |
68 | 61, 64, 67 | 3anbi123d 1399 |
. . . . . . . . . . 11
..^
..^
..^ ..^
..^ ..^ ..^ ..^ |
69 | 55, 68 | ralbida 2982 |
. . . . . . . . . 10
..^
..^
..^ ..^ ..^ ..^ ..^ ..^ ..^ |
70 | 69 | anbi1d 741 |
. . . . . . . . 9
..^
..^
..^ ..^
..^ ..^
..^ ..^
..^ |
71 | 70 | 2rexbidva 3056 |
. . . . . . . 8
..^
..^
..^ ..^
..^ ..^
..^ ..^
..^ |
72 | 51, 71 | anbi12d 747 |
. . . . . . 7
..^ ..^
..^ ..^ ..^
..^ ..^ ..^ ..^ ..^ ..^ ..^ |
73 | 50, 72 | spcev 3300 |
. . . . . 6
..^ ..^
..^ ..^ ..^ ..^ ..^ ..^ ..^ ..^
..^
|
74 | 41, 48, 73 | syl2an 494 |
. . . . 5
..^
..^ |
75 | 21, 74 | impbida 877 |
. . . 4
..^
..^
|
76 | 75 | rexbiia 3040 |
. . 3
..^
..^
|
77 | 14, 15, 76 | 3bitr2i 288 |
. 2
..^
..^
|
78 | 8, 77 | syl6bb 276 |
1
DimTarskiG≥
|