Step | Hyp | Ref
| Expression |
1 | | isucn2.1 |
. . 3
UnifOn |
2 | | isucn2.2 |
. . 3
UnifOn |
3 | | isucn 22082 |
. . 3
UnifOn UnifOn
Cnu
|
4 | 1, 2, 3 | syl2anc 693 |
. 2
Cnu
|
5 | | isucn2.4 |
. . . . . . . . . . . 12
|
6 | | ssfg 21676 |
. . . . . . . . . . . 12
|
7 | 5, 6 | syl 17 |
. . . . . . . . . . 11
|
8 | | isucn2.v |
. . . . . . . . . . 11
|
9 | 7, 8 | syl6sseqr 3652 |
. . . . . . . . . 10
|
10 | 9 | adantr 481 |
. . . . . . . . 9
|
11 | 10 | adantr 481 |
. . . . . . . 8
|
12 | 11 | sselda 3603 |
. . . . . . 7
|
13 | | simplr 792 |
. . . . . . 7
|
14 | | breq 4655 |
. . . . . . . . . . 11
|
15 | 14 | imbi2d 330 |
. . . . . . . . . 10
|
16 | 15 | ralbidv 2986 |
. . . . . . . . 9
|
17 | 16 | rexralbidv 3058 |
. . . . . . . 8
|
18 | 17 | rspcva 3307 |
. . . . . . 7
|
19 | 12, 13, 18 | syl2anc 693 |
. . . . . 6
|
20 | | simpr 477 |
. . . . . . . . . . . 12
|
21 | | isucn2.u |
. . . . . . . . . . . 12
|
22 | 20, 21 | syl6eleq 2711 |
. . . . . . . . . . 11
|
23 | | isucn2.3 |
. . . . . . . . . . . . 13
|
24 | | elfg 21675 |
. . . . . . . . . . . . 13
|
25 | 23, 24 | syl 17 |
. . . . . . . . . . . 12
|
26 | 25 | simplbda 654 |
. . . . . . . . . . 11
|
27 | 22, 26 | syldan 487 |
. . . . . . . . . 10
|
28 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
|
29 | 28 | ssbrd 4696 |
. . . . . . . . . . . . . . . . . 18
|
30 | 29 | imim1d 82 |
. . . . . . . . . . . . . . . . 17
|
31 | 30 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
32 | 31 | ralrimivw 2967 |
. . . . . . . . . . . . . . 15
|
33 | 32 | ralrimivw 2967 |
. . . . . . . . . . . . . 14
|
34 | | ralim 2948 |
. . . . . . . . . . . . . . 15
|
35 | 34 | ralimi 2952 |
. . . . . . . . . . . . . 14
|
36 | | ralim 2948 |
. . . . . . . . . . . . . 14
|
37 | 33, 35, 36 | 3syl 18 |
. . . . . . . . . . . . 13
|
38 | 37 | ex 450 |
. . . . . . . . . . . 12
|
39 | 38 | reximdva 3017 |
. . . . . . . . . . 11
|
40 | 39 | adantr 481 |
. . . . . . . . . 10
|
41 | 27, 40 | mpd 15 |
. . . . . . . . 9
|
42 | | r19.37v 3087 |
. . . . . . . . 9
|
43 | 41, 42 | syl 17 |
. . . . . . . 8
|
44 | 43 | rexlimdva 3031 |
. . . . . . 7
|
45 | 44 | ad3antrrr 766 |
. . . . . 6
|
46 | 19, 45 | mpd 15 |
. . . . 5
|
47 | 46 | ralrimiva 2966 |
. . . 4
|
48 | | ssfg 21676 |
. . . . . . . . . . 11
|
49 | 23, 48 | syl 17 |
. . . . . . . . . 10
|
50 | 49, 21 | syl6sseqr 3652 |
. . . . . . . . 9
|
51 | | ssrexv 3667 |
. . . . . . . . . 10
|
52 | | breq 4655 |
. . . . . . . . . . . . 13
|
53 | 52 | imbi1d 331 |
. . . . . . . . . . . 12
|
54 | 53 | 2ralbidv 2989 |
. . . . . . . . . . 11
|
55 | 54 | cbvrexv 3172 |
. . . . . . . . . 10
|
56 | 51, 55 | syl6ib 241 |
. . . . . . . . 9
|
57 | 50, 56 | syl 17 |
. . . . . . . 8
|
58 | 57 | ralimdv 2963 |
. . . . . . 7
|
59 | 58 | adantr 481 |
. . . . . 6
|
60 | | nfv 1843 |
. . . . . . . . . . 11
|
61 | | nfra1 2941 |
. . . . . . . . . . 11
|
62 | 60, 61 | nfan 1828 |
. . . . . . . . . 10
|
63 | | nfv 1843 |
. . . . . . . . . 10
|
64 | 62, 63 | nfan 1828 |
. . . . . . . . 9
|
65 | | simp-4r 807 |
. . . . . . . . . . 11
|
66 | | simplr 792 |
. . . . . . . . . . 11
|
67 | | rspa 2930 |
. . . . . . . . . . 11
|
68 | 65, 66, 67 | syl2anc 693 |
. . . . . . . . . 10
|
69 | | simp-4l 806 |
. . . . . . . . . . 11
|
70 | | simpr 477 |
. . . . . . . . . . 11
|
71 | | id 22 |
. . . . . . . . . . . . . . . . 17
|
72 | 71 | ssbrd 4696 |
. . . . . . . . . . . . . . . 16
|
73 | 72 | adantl 482 |
. . . . . . . . . . . . . . 15
|
74 | 73 | imim2d 57 |
. . . . . . . . . . . . . 14
|
75 | 74 | ralimdv 2963 |
. . . . . . . . . . . . 13
|
76 | 75 | ralimdv 2963 |
. . . . . . . . . . . 12
|
77 | 76 | reximdv 3016 |
. . . . . . . . . . 11
|
78 | 69, 66, 70, 77 | syl21anc 1325 |
. . . . . . . . . 10
|
79 | 68, 78 | mpd 15 |
. . . . . . . . 9
|
80 | 5 | ad3antrrr 766 |
. . . . . . . . . 10
|
81 | | simpr 477 |
. . . . . . . . . . 11
|
82 | 81, 8 | syl6eleq 2711 |
. . . . . . . . . 10
|
83 | | elfg 21675 |
. . . . . . . . . . 11
|
84 | 83 | simplbda 654 |
. . . . . . . . . 10
|
85 | 80, 82, 84 | syl2anc 693 |
. . . . . . . . 9
|
86 | 64, 79, 85 | r19.29af 3076 |
. . . . . . . 8
|
87 | 86 | ralrimiva 2966 |
. . . . . . 7
|
88 | 87 | ex 450 |
. . . . . 6
|
89 | 59, 88 | syld 47 |
. . . . 5
|
90 | 89 | imp 445 |
. . . 4
|
91 | 47, 90 | impbida 877 |
. . 3
|
92 | 91 | pm5.32da 673 |
. 2
|
93 | 4, 92 | bitrd 268 |
1
Cnu
|