Step | Hyp | Ref
| Expression |
1 | | tru 1487 |
. . . 4
|
2 | | eqeq12 2635 |
. . . . . 6
|
3 | | csbeq1 3536 |
. . . . . . . 8
..^ ..^ |
4 | | csbeq1 3536 |
. . . . . . . 8
..^ ..^ |
5 | 3, 4 | ineqan12d 3816 |
. . . . . . 7
..^ ..^
..^
..^ |
6 | 5 | eqeq1d 2624 |
. . . . . 6
..^ ..^
..^
..^ |
7 | 2, 6 | orbi12d 746 |
. . . . 5
..^ ..^ ..^ ..^ |
8 | | eqeq12 2635 |
. . . . . . 7
|
9 | | equcom 1945 |
. . . . . . 7
|
10 | 8, 9 | syl6bb 276 |
. . . . . 6
|
11 | | csbeq1 3536 |
. . . . . . . . 9
..^ ..^ |
12 | | csbeq1 3536 |
. . . . . . . . 9
..^ ..^ |
13 | 11, 12 | ineqan12d 3816 |
. . . . . . . 8
..^ ..^
..^
..^ |
14 | | incom 3805 |
. . . . . . . 8
..^ ..^
..^
..^ |
15 | 13, 14 | syl6eq 2672 |
. . . . . . 7
..^ ..^
..^
..^ |
16 | 15 | eqeq1d 2624 |
. . . . . 6
..^ ..^
..^
..^ |
17 | 10, 16 | orbi12d 746 |
. . . . 5
..^ ..^ ..^ ..^ |
18 | | nnssre 11024 |
. . . . . 6
|
19 | 18 | a1i 11 |
. . . . 5
|
20 | | biidd 252 |
. . . . 5
..^ ..^ ..^ ..^ |
21 | | nesym 2850 |
. . . . . . . 8
|
22 | | nnre 11027 |
. . . . . . . . . 10
|
23 | | nnre 11027 |
. . . . . . . . . 10
|
24 | | id 22 |
. . . . . . . . . 10
|
25 | | leltne 10127 |
. . . . . . . . . 10
|
26 | 22, 23, 24, 25 | syl3an 1368 |
. . . . . . . . 9
|
27 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
28 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . 16
|
29 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
..^ |
30 | | iundisjf.2 |
. . . . . . . . . . . . . . . . 17
|
31 | 29, 30 | nfiun 4548 |
. . . . . . . . . . . . . . . 16
..^ |
32 | 28, 31 | nfdif 3731 |
. . . . . . . . . . . . . . 15
..^ |
33 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . 16
|
34 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
35 | 34 | iuneq1d 4545 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
36 | 33, 35 | difeq12d 3729 |
. . . . . . . . . . . . . . 15
..^
..^ |
37 | 27, 32, 36 | csbief 3558 |
. . . . . . . . . . . . . 14
..^ ..^ |
38 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
39 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . 16
|
40 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
..^ |
41 | 40, 30 | nfiun 4548 |
. . . . . . . . . . . . . . . 16
..^ |
42 | 39, 41 | nfdif 3731 |
. . . . . . . . . . . . . . 15
..^ |
43 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . 16
|
44 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
45 | 44 | iuneq1d 4545 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
46 | 43, 45 | difeq12d 3729 |
. . . . . . . . . . . . . . 15
..^
..^ |
47 | 38, 42, 46 | csbief 3558 |
. . . . . . . . . . . . . 14
..^ ..^ |
48 | 37, 47 | ineq12i 3812 |
. . . . . . . . . . . . 13
..^ ..^
..^
..^ |
49 | | simp1 1061 |
. . . . . . . . . . . . . . . . . 18
|
50 | | nnuz 11723 |
. . . . . . . . . . . . . . . . . 18
|
51 | 49, 50 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . 17
|
52 | | simp2 1062 |
. . . . . . . . . . . . . . . . . 18
|
53 | 52 | nnzd 11481 |
. . . . . . . . . . . . . . . . 17
|
54 | | simp3 1063 |
. . . . . . . . . . . . . . . . 17
|
55 | | elfzo2 12473 |
. . . . . . . . . . . . . . . . 17
..^
|
56 | 51, 53, 54, 55 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . 16
..^ |
57 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
..^ |
58 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
|
59 | | iundisjf.1 |
. . . . . . . . . . . . . . . . . 18
|
60 | 58, 59 | nfcsb 3551 |
. . . . . . . . . . . . . . . . 17
|
61 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . 20
|
62 | | iundisjf.3 |
. . . . . . . . . . . . . . . . . . . 20
|
63 | 61, 30, 62 | csbhypf 3552 |
. . . . . . . . . . . . . . . . . . 19
|
64 | 63 | equcoms 1947 |
. . . . . . . . . . . . . . . . . 18
|
65 | 64 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
|
66 | 57, 58, 60, 65 | ssiun2sf 29378 |
. . . . . . . . . . . . . . . 16
..^
..^ |
67 | 56, 66 | syl 17 |
. . . . . . . . . . . . . . 15
..^ |
68 | 67 | ssdifssd 3748 |
. . . . . . . . . . . . . 14
..^ ..^ |
69 | | ssrin 3838 |
. . . . . . . . . . . . . 14
..^ ..^
..^
..^ ..^
..^ |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . 13
..^
..^ ..^
..^ |
71 | 48, 70 | syl5eqss 3649 |
. . . . . . . . . . . 12
..^
..^
..^
..^ |
72 | | disjdif 4040 |
. . . . . . . . . . . 12
..^
..^ |
73 | | sseq0 3975 |
. . . . . . . . . . . 12
..^ ..^
..^
..^
..^
..^ ..^ ..^ |
74 | 71, 72, 73 | sylancl 694 |
. . . . . . . . . . 11
..^
..^ |
75 | 74 | 3expia 1267 |
. . . . . . . . . 10
..^ ..^ |
76 | 75 | 3adant3 1081 |
. . . . . . . . 9
..^
..^ |
77 | 26, 76 | sylbird 250 |
. . . . . . . 8
..^
..^ |
78 | 21, 77 | syl5bir 233 |
. . . . . . 7
..^ ..^ |
79 | 78 | orrd 393 |
. . . . . 6
..^ ..^ |
80 | 79 | adantl 482 |
. . . . 5
..^ ..^ |
81 | 7, 17, 19, 20, 80 | wlogle 10561 |
. . . 4
..^ ..^ |
82 | 1, 81 | mpan 706 |
. . 3
..^ ..^ |
83 | 82 | rgen2a 2977 |
. 2
..^ ..^ |
84 | | disjors 4635 |
. 2
Disj
..^
..^ ..^ |
85 | 83, 84 | mpbir 221 |
1
Disj
..^ |