Step | Hyp | Ref
| Expression |
1 | | cicrcl 16463 |
. 2
𝑐
|
2 | | ciclcl 16462 |
. 2
𝑐
|
3 | | eqid 2622 |
. . . . 5
|
4 | | eqid 2622 |
. . . . 5
|
5 | | simpl 473 |
. . . . 5
|
6 | | simpr 477 |
. . . . . 6
|
7 | 6 | adantl 482 |
. . . . 5
|
8 | | simpl 473 |
. . . . . 6
|
9 | 8 | adantl 482 |
. . . . 5
|
10 | 3, 4, 5, 7, 9 | cic 16459 |
. . . 4
𝑐
|
11 | | eqid 2622 |
. . . . . . . . . . . 12
Inv Inv |
12 | 4, 11, 5, 7, 9, 3 | isoval 16425 |
. . . . . . . . . . 11
Inv |
13 | 4, 11, 5, 9, 7 | invsym2 16423 |
. . . . . . . . . . . . . 14
Inv Inv |
14 | 13 | eqcomd 2628 |
. . . . . . . . . . . . 13
Inv Inv |
15 | 14 | dmeqd 5326 |
. . . . . . . . . . . 12
Inv Inv |
16 | | df-rn 5125 |
. . . . . . . . . . . 12
Inv Inv |
17 | 15, 16 | syl6eqr 2674 |
. . . . . . . . . . 11
Inv Inv |
18 | 12, 17 | eqtrd 2656 |
. . . . . . . . . 10
Inv |
19 | 18 | eleq2d 2687 |
. . . . . . . . 9
Inv |
20 | | vex 3203 |
. . . . . . . . . 10
|
21 | | elrng 5314 |
. . . . . . . . . 10
Inv
Inv |
22 | 20, 21 | mp1i 13 |
. . . . . . . . 9
Inv Inv |
23 | 19, 22 | bitrd 268 |
. . . . . . . 8
Inv |
24 | | df-br 4654 |
. . . . . . . . . 10
Inv Inv |
25 | 24 | exbii 1774 |
. . . . . . . . 9
Inv
Inv |
26 | | vex 3203 |
. . . . . . . . . . . . 13
|
27 | 26, 20 | opeldm 5328 |
. . . . . . . . . . . 12
Inv Inv |
28 | 4, 11, 5, 9, 7, 3 | isoval 16425 |
. . . . . . . . . . . . . . . 16
Inv |
29 | 28 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
Inv |
30 | 29 | eleq2d 2687 |
. . . . . . . . . . . . . 14
Inv |
31 | 5 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
32 | 9 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
33 | 7 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
34 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
35 | 3, 4, 31, 32, 33, 34 | brcici 16460 |
. . . . . . . . . . . . . . 15
𝑐 |
36 | 35 | ex 450 |
. . . . . . . . . . . . . 14
𝑐 |
37 | 30, 36 | sylbid 230 |
. . . . . . . . . . . . 13
Inv
𝑐 |
38 | 37 | com12 32 |
. . . . . . . . . . . 12
Inv
𝑐 |
39 | 27, 38 | syl 17 |
. . . . . . . . . . 11
Inv
𝑐
|
40 | 39 | exlimiv 1858 |
. . . . . . . . . 10
Inv
𝑐
|
41 | 40 | com12 32 |
. . . . . . . . 9
Inv 𝑐 |
42 | 25, 41 | syl5bi 232 |
. . . . . . . 8
Inv 𝑐 |
43 | 23, 42 | sylbid 230 |
. . . . . . 7
𝑐 |
44 | 43 | com12 32 |
. . . . . 6
𝑐 |
45 | 44 | exlimiv 1858 |
. . . . 5
𝑐 |
46 | 45 | com12 32 |
. . . 4
𝑐
|
47 | 10, 46 | sylbid 230 |
. . 3
𝑐 𝑐
|
48 | 47 | impancom 456 |
. 2
𝑐
𝑐 |
49 | 1, 2, 48 | mp2and 715 |
1
𝑐
𝑐 |