Proof of Theorem cnvrcl0
Step | Hyp | Ref
| Expression |
1 | | cnvresid 5968 |
. . . . . . 7
|
2 | | cnvnonrel 37894 |
. . . . . . . . . . . . . . . 16
|
3 | | cnv0 5535 |
. . . . . . . . . . . . . . . 16
|
4 | 2, 3 | eqtr4i 2647 |
. . . . . . . . . . . . . . 15
|
5 | 4 | dmeqi 5325 |
. . . . . . . . . . . . . 14
|
6 | | df-rn 5125 |
. . . . . . . . . . . . . 14
|
7 | | df-rn 5125 |
. . . . . . . . . . . . . 14
|
8 | 5, 6, 7 | 3eqtr4i 2654 |
. . . . . . . . . . . . 13
|
9 | | 0ss 3972 |
. . . . . . . . . . . . . 14
|
10 | | rnss 5354 |
. . . . . . . . . . . . . 14
|
11 | 9, 10 | ax-mp 5 |
. . . . . . . . . . . . 13
|
12 | 8, 11 | eqsstri 3635 |
. . . . . . . . . . . 12
|
13 | | ssequn2 3786 |
. . . . . . . . . . . 12
|
14 | 12, 13 | mpbi 220 |
. . . . . . . . . . 11
|
15 | | rnun 5541 |
. . . . . . . . . . 11
|
16 | | dfdm4 5316 |
. . . . . . . . . . 11
|
17 | 14, 15, 16 | 3eqtr4ri 2655 |
. . . . . . . . . 10
|
18 | 4 | rneqi 5352 |
. . . . . . . . . . . . . 14
|
19 | | dfdm4 5316 |
. . . . . . . . . . . . . 14
|
20 | | dfdm4 5316 |
. . . . . . . . . . . . . 14
|
21 | 18, 19, 20 | 3eqtr4i 2654 |
. . . . . . . . . . . . 13
|
22 | | dmss 5323 |
. . . . . . . . . . . . . 14
|
23 | 9, 22 | ax-mp 5 |
. . . . . . . . . . . . 13
|
24 | 21, 23 | eqsstri 3635 |
. . . . . . . . . . . 12
|
25 | | ssequn2 3786 |
. . . . . . . . . . . 12
|
26 | 24, 25 | mpbi 220 |
. . . . . . . . . . 11
|
27 | | dmun 5331 |
. . . . . . . . . . 11
|
28 | | df-rn 5125 |
. . . . . . . . . . 11
|
29 | 26, 27, 28 | 3eqtr4ri 2655 |
. . . . . . . . . 10
|
30 | 17, 29 | uneq12i 3765 |
. . . . . . . . 9
|
31 | 30 | equncomi 3759 |
. . . . . . . 8
|
32 | 31 | reseq2i 5393 |
. . . . . . 7
|
33 | 1, 32 | eqtr2i 2645 |
. . . . . 6
|
34 | | cnvss 5294 |
. . . . . 6
|
35 | 33, 34 | syl5eqss 3649 |
. . . . 5
|
36 | | ssun1 3776 |
. . . . 5
|
37 | 35, 36 | syl6ss 3615 |
. . . 4
|
38 | | dmeq 5324 |
. . . . . . 7
|
39 | | rneq 5351 |
. . . . . . 7
|
40 | 38, 39 | uneq12d 3768 |
. . . . . 6
|
41 | 40 | reseq2d 5396 |
. . . . 5
|
42 | | id 22 |
. . . . 5
|
43 | 41, 42 | sseq12d 3634 |
. . . 4
|
44 | 37, 43 | syl5ibr 236 |
. . 3
|
45 | 44 | adantl 482 |
. 2
|
46 | | cnvresid 5968 |
. . . . . 6
|
47 | | dfdm4 5316 |
. . . . . . . . 9
|
48 | | df-rn 5125 |
. . . . . . . . 9
|
49 | 47, 48 | uneq12i 3765 |
. . . . . . . 8
|
50 | 49 | equncomi 3759 |
. . . . . . 7
|
51 | 50 | reseq2i 5393 |
. . . . . 6
|
52 | 46, 51 | eqtr2i 2645 |
. . . . 5
|
53 | | cnvss 5294 |
. . . . 5
|
54 | 52, 53 | syl5eqss 3649 |
. . . 4
|
55 | | dmeq 5324 |
. . . . . . 7
|
56 | | rneq 5351 |
. . . . . . 7
|
57 | 55, 56 | uneq12d 3768 |
. . . . . 6
|
58 | 57 | reseq2d 5396 |
. . . . 5
|
59 | | id 22 |
. . . . 5
|
60 | 58, 59 | sseq12d 3634 |
. . . 4
|
61 | 54, 60 | syl5ibr 236 |
. . 3
|
62 | 61 | adantl 482 |
. 2
|
63 | | dmeq 5324 |
. . . . 5
|
64 | | rneq 5351 |
. . . . 5
|
65 | 63, 64 | uneq12d 3768 |
. . . 4
|
66 | 65 | reseq2d 5396 |
. . 3
|
67 | | id 22 |
. . 3
|
68 | 66, 67 | sseq12d 3634 |
. 2
|
69 | | ssun1 3776 |
. . 3
|
70 | 69 | a1i 11 |
. 2
|
71 | | dmexg 7097 |
. . . . 5
|
72 | | rnexg 7098 |
. . . . 5
|
73 | | unexg 6959 |
. . . . 5
|
74 | 71, 72, 73 | syl2anc 693 |
. . . 4
|
75 | 74 | resiexd 6480 |
. . 3
|
76 | | unexg 6959 |
. . 3
|
77 | 75, 76 | mpdan 702 |
. 2
|
78 | | dmun 5331 |
. . . . . 6
|
79 | | ssun1 3776 |
. . . . . . 7
|
80 | | dmresi 5457 |
. . . . . . . 8
|
81 | 80 | eqimssi 3659 |
. . . . . . 7
|
82 | 79, 81 | unssi 3788 |
. . . . . 6
|
83 | 78, 82 | eqsstri 3635 |
. . . . 5
|
84 | | rnun 5541 |
. . . . . 6
|
85 | | ssun2 3777 |
. . . . . . 7
|
86 | | rnresi 5479 |
. . . . . . . 8
|
87 | 86 | eqimssi 3659 |
. . . . . . 7
|
88 | 85, 87 | unssi 3788 |
. . . . . 6
|
89 | 84, 88 | eqsstri 3635 |
. . . . 5
|
90 | 83, 89 | pm3.2i 471 |
. . . 4
|
91 | | unss 3787 |
. . . . 5
|
92 | | ssres2 5425 |
. . . . 5
|
93 | 91, 92 | sylbi 207 |
. . . 4
|
94 | | ssun4 3779 |
. . . 4
|
95 | 90, 93, 94 | mp2b 10 |
. . 3
|
96 | 95 | a1i 11 |
. 2
|
97 | 45, 62, 68, 70, 77, 96 | clcnvlem 37930 |
1
|