Step | Hyp | Ref
| Expression |
1 | | uniiun 4573 |
. . 3
|
2 | 1 | a1i 11 |
. 2
|
3 | | simpl 473 |
. . . . . . 7
|
4 | | elun1 3780 |
. . . . . . . 8
|
5 | 4 | adantl 482 |
. . . . . . 7
|
6 | | foelrni 6244 |
. . . . . . 7
|
7 | 3, 5, 6 | syl2anc 693 |
. . . . . 6
|
8 | | eqimss2 3658 |
. . . . . . 7
|
9 | 8 | reximi 3011 |
. . . . . 6
|
10 | 7, 9 | syl 17 |
. . . . 5
|
11 | 10 | ralrimiva 2966 |
. . . 4
|
12 | | iunss2 4565 |
. . . 4
|
13 | 11, 12 | syl 17 |
. . 3
|
14 | | simpl 473 |
. . . . . 6
|
15 | | uneq1 3760 |
. . . . . . . . 9
|
16 | | 0un 39215 |
. . . . . . . . . 10
|
17 | 16 | a1i 11 |
. . . . . . . . 9
|
18 | 15, 17 | eqtrd 2656 |
. . . . . . . 8
|
19 | 18 | adantl 482 |
. . . . . . 7
|
20 | | foeq3 6113 |
. . . . . . 7
|
21 | 19, 20 | syl 17 |
. . . . . 6
|
22 | 14, 21 | mpbid 222 |
. . . . 5
|
23 | | unisn0 39222 |
. . . . . . . . 9
|
24 | 23 | eqcomi 2631 |
. . . . . . . 8
|
25 | 24 | a1i 11 |
. . . . . . 7
|
26 | | founiiun 39360 |
. . . . . . 7
|
27 | 25, 26 | eqtr2d 2657 |
. . . . . 6
|
28 | | 0ss 3972 |
. . . . . . 7
|
29 | 28 | a1i 11 |
. . . . . 6
|
30 | 27, 29 | eqsstrd 3639 |
. . . . 5
|
31 | 22, 30 | syl 17 |
. . . 4
|
32 | | ssid 3624 |
. . . . . . . . 9
|
33 | | sseq2 3627 |
. . . . . . . . . 10
|
34 | 33 | rspcev 3309 |
. . . . . . . . 9
|
35 | 32, 34 | mpan2 707 |
. . . . . . . 8
|
36 | 35 | adantl 482 |
. . . . . . 7
|
37 | | simpl 473 |
. . . . . . . 8
|
38 | | fof 6115 |
. . . . . . . . . . . . 13
|
39 | 38 | ffvelrnda 6359 |
. . . . . . . . . . . 12
|
40 | 39 | adantr 481 |
. . . . . . . . . . 11
|
41 | | simpr 477 |
. . . . . . . . . . 11
|
42 | | elunnel1 3754 |
. . . . . . . . . . 11
|
43 | 40, 41, 42 | syl2anc 693 |
. . . . . . . . . 10
|
44 | | elsni 4194 |
. . . . . . . . . 10
|
45 | 43, 44 | syl 17 |
. . . . . . . . 9
|
46 | 45 | adantllr 755 |
. . . . . . . 8
|
47 | | neq0 3930 |
. . . . . . . . . . . . 13
|
48 | 47 | biimpi 206 |
. . . . . . . . . . . 12
|
49 | 48 | adantr 481 |
. . . . . . . . . . 11
|
50 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
51 | | id 22 |
. . . . . . . . . . . . . . . . 17
|
52 | | 0ss 3972 |
. . . . . . . . . . . . . . . . . 18
|
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
54 | 51, 53 | eqsstrd 3639 |
. . . . . . . . . . . . . . . 16
|
55 | 54 | adantr 481 |
. . . . . . . . . . . . . . 15
|
56 | 50, 55 | jca 554 |
. . . . . . . . . . . . . 14
|
57 | 56 | ex 450 |
. . . . . . . . . . . . 13
|
58 | 57 | adantl 482 |
. . . . . . . . . . . 12
|
59 | 58 | eximdv 1846 |
. . . . . . . . . . 11
|
60 | 49, 59 | mpd 15 |
. . . . . . . . . 10
|
61 | | df-rex 2918 |
. . . . . . . . . 10
|
62 | 60, 61 | sylibr 224 |
. . . . . . . . 9
|
63 | 62 | ad4ant24 1298 |
. . . . . . . 8
|
64 | 37, 46, 63 | syl2anc 693 |
. . . . . . 7
|
65 | 36, 64 | pm2.61dan 832 |
. . . . . 6
|
66 | 65 | ralrimiva 2966 |
. . . . 5
|
67 | | iunss2 4565 |
. . . . 5
|
68 | 66, 67 | syl 17 |
. . . 4
|
69 | 31, 68 | pm2.61dan 832 |
. . 3
|
70 | 13, 69 | eqssd 3620 |
. 2
|
71 | 2, 70 | eqtrd 2656 |
1
|