Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . 5
|
2 | 1 | iscmp 21191 |
. . . 4
|
3 | 2 | simprbi 480 |
. . 3
|
4 | | unitg 20771 |
. . . . . . . 8
|
5 | | eqtr3 2643 |
. . . . . . . 8
|
6 | 4, 5 | sylan 488 |
. . . . . . 7
|
7 | 6 | eqeq1d 2624 |
. . . . . 6
|
8 | 6 | eqeq1d 2624 |
. . . . . . 7
|
9 | 8 | rexbidv 3052 |
. . . . . 6
|
10 | 7, 9 | imbi12d 334 |
. . . . 5
|
11 | 10 | ralbidv 2986 |
. . . 4
|
12 | | bastg 20770 |
. . . . . . 7
|
13 | 12 | adantr 481 |
. . . . . 6
|
14 | | sspwb 4917 |
. . . . . 6
|
15 | 13, 14 | sylib 208 |
. . . . 5
|
16 | | ssralv 3666 |
. . . . 5
|
17 | 15, 16 | syl 17 |
. . . 4
|
18 | 11, 17 | sylbid 230 |
. . 3
|
19 | 3, 18 | syl5 34 |
. 2
|
20 | | elpwi 4168 |
. . . . 5
|
21 | | simprr 796 |
. . . . . . . . . . 11
|
22 | | simprl 794 |
. . . . . . . . . . . . . . . . . 18
|
23 | 22 | sselda 3603 |
. . . . . . . . . . . . . . . . 17
|
24 | 23 | adantrr 753 |
. . . . . . . . . . . . . . . 16
|
25 | | simprr 796 |
. . . . . . . . . . . . . . . 16
|
26 | | tg2 20769 |
. . . . . . . . . . . . . . . 16
|
27 | 24, 25, 26 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
28 | 27 | expr 643 |
. . . . . . . . . . . . . 14
|
29 | 28 | reximdva 3017 |
. . . . . . . . . . . . 13
|
30 | | eluni2 4440 |
. . . . . . . . . . . . 13
|
31 | | elunirab 4448 |
. . . . . . . . . . . . . 14
|
32 | | r19.42v 3092 |
. . . . . . . . . . . . . . 15
|
33 | 32 | rexbii 3041 |
. . . . . . . . . . . . . 14
|
34 | | rexcom 3099 |
. . . . . . . . . . . . . 14
|
35 | 31, 33, 34 | 3bitr2i 288 |
. . . . . . . . . . . . 13
|
36 | 29, 30, 35 | 3imtr4g 285 |
. . . . . . . . . . . 12
|
37 | 36 | ssrdv 3609 |
. . . . . . . . . . 11
|
38 | 21, 37 | eqsstrd 3639 |
. . . . . . . . . 10
|
39 | | ssrab2 3687 |
. . . . . . . . . . . 12
|
40 | 39 | unissi 4461 |
. . . . . . . . . . 11
|
41 | | simplr 792 |
. . . . . . . . . . 11
|
42 | 40, 41 | syl5sseqr 3654 |
. . . . . . . . . 10
|
43 | 38, 42 | eqssd 3620 |
. . . . . . . . 9
|
44 | | elpw2g 4827 |
. . . . . . . . . . . 12
|
45 | 44 | ad2antrr 762 |
. . . . . . . . . . 11
|
46 | 39, 45 | mpbiri 248 |
. . . . . . . . . 10
|
47 | | unieq 4444 |
. . . . . . . . . . . . 13
|
48 | 47 | eqeq2d 2632 |
. . . . . . . . . . . 12
|
49 | | pweq 4161 |
. . . . . . . . . . . . . 14
|
50 | 49 | ineq1d 3813 |
. . . . . . . . . . . . 13
|
51 | 50 | rexeqdv 3145 |
. . . . . . . . . . . 12
|
52 | 48, 51 | imbi12d 334 |
. . . . . . . . . . 11
|
53 | 52 | rspcv 3305 |
. . . . . . . . . 10
|
54 | 46, 53 | syl 17 |
. . . . . . . . 9
|
55 | 43, 54 | mpid 44 |
. . . . . . . 8
|
56 | | elfpw 8268 |
. . . . . . . . . . . . 13
|
57 | 56 | simprbi 480 |
. . . . . . . . . . . 12
|
58 | 57 | ad2antrl 764 |
. . . . . . . . . . 11
|
59 | 56 | simplbi 476 |
. . . . . . . . . . . . 13
|
60 | 59 | ad2antrl 764 |
. . . . . . . . . . . 12
|
61 | | ssrab 3680 |
. . . . . . . . . . . . 13
|
62 | 61 | simprbi 480 |
. . . . . . . . . . . 12
|
63 | 60, 62 | syl 17 |
. . . . . . . . . . 11
|
64 | | sseq2 3627 |
. . . . . . . . . . . 12
|
65 | 64 | ac6sfi 8204 |
. . . . . . . . . . 11
|
66 | 58, 63, 65 | syl2anc 693 |
. . . . . . . . . 10
|
67 | | frn 6053 |
. . . . . . . . . . . . 13
|
68 | 67 | ad2antrl 764 |
. . . . . . . . . . . 12
|
69 | | ffn 6045 |
. . . . . . . . . . . . . . 15
|
70 | | dffn4 6121 |
. . . . . . . . . . . . . . 15
|
71 | 69, 70 | sylib 208 |
. . . . . . . . . . . . . 14
|
72 | 71 | adantr 481 |
. . . . . . . . . . . . 13
|
73 | | fofi 8252 |
. . . . . . . . . . . . 13
|
74 | 58, 72, 73 | syl2an 494 |
. . . . . . . . . . . 12
|
75 | | elfpw 8268 |
. . . . . . . . . . . 12
|
76 | 68, 74, 75 | sylanbrc 698 |
. . . . . . . . . . 11
|
77 | | simplrr 801 |
. . . . . . . . . . . . 13
|
78 | | uniiun 4573 |
. . . . . . . . . . . . . . . 16
|
79 | | ss2iun 4536 |
. . . . . . . . . . . . . . . 16
|
80 | 78, 79 | syl5eqss 3649 |
. . . . . . . . . . . . . . 15
|
81 | 80 | ad2antll 765 |
. . . . . . . . . . . . . 14
|
82 | | fniunfv 6505 |
. . . . . . . . . . . . . . . 16
|
83 | 69, 82 | syl 17 |
. . . . . . . . . . . . . . 15
|
84 | 83 | ad2antrl 764 |
. . . . . . . . . . . . . 14
|
85 | 81, 84 | sseqtrd 3641 |
. . . . . . . . . . . . 13
|
86 | 77, 85 | eqsstrd 3639 |
. . . . . . . . . . . 12
|
87 | 68 | unissd 4462 |
. . . . . . . . . . . . 13
|
88 | 21 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
89 | 87, 88 | sseqtr4d 3642 |
. . . . . . . . . . . 12
|
90 | 86, 89 | eqssd 3620 |
. . . . . . . . . . 11
|
91 | | unieq 4444 |
. . . . . . . . . . . . 13
|
92 | 91 | eqeq2d 2632 |
. . . . . . . . . . . 12
|
93 | 92 | rspcev 3309 |
. . . . . . . . . . 11
|
94 | 76, 90, 93 | syl2anc 693 |
. . . . . . . . . 10
|
95 | 66, 94 | exlimddv 1863 |
. . . . . . . . 9
|
96 | 95 | rexlimdvaa 3032 |
. . . . . . . 8
|
97 | 55, 96 | syld 47 |
. . . . . . 7
|
98 | 97 | expr 643 |
. . . . . 6
|
99 | 98 | com23 86 |
. . . . 5
|
100 | 20, 99 | sylan2 491 |
. . . 4
|
101 | 100 | ralrimdva 2969 |
. . 3
|
102 | | tgcl 20773 |
. . . . . 6
|
103 | 102 | adantr 481 |
. . . . 5
|
104 | 1 | iscmp 21191 |
. . . . . 6
|
105 | 104 | baib 944 |
. . . . 5
|
106 | 103, 105 | syl 17 |
. . . 4
|
107 | 6 | eqeq1d 2624 |
. . . . . 6
|
108 | 6 | eqeq1d 2624 |
. . . . . . 7
|
109 | 108 | rexbidv 3052 |
. . . . . 6
|
110 | 107, 109 | imbi12d 334 |
. . . . 5
|
111 | 110 | ralbidv 2986 |
. . . 4
|
112 | 106, 111 | bitrd 268 |
. . 3
|
113 | 101, 112 | sylibrd 249 |
. 2
|
114 | 19, 113 | impbid 202 |
1
|