Step | Hyp | Ref
| Expression |
1 | | df-addcfn 5746 |
. . 3
AddC
|
2 | | elin 3219 |
. . . . . . . 8
Ins2 Ins2 S Ins4 Ins2 Ins2
S Ins4 SI3 Ins3 Disj Cup 1c
Ins2 Ins2
S Ins4 Ins2 Ins2 S Ins4 SI3 Ins3 Disj Cup 1c |
3 | | snex 4111 |
. . . . . . . . . . 11
|
4 | 3 | otelins2 5791 |
. . . . . . . . . 10
Ins2 Ins2
S Ins2
S |
5 | | vex 2862 |
. . . . . . . . . . 11
|
6 | 5 | otelins2 5791 |
. . . . . . . . . 10
Ins2
S
S |
7 | | vex 2862 |
. . . . . . . . . . 11
|
8 | | vex 2862 |
. . . . . . . . . . 11
|
9 | 7, 8 | opelssetsn 4760 |
. . . . . . . . . 10
S |
10 | 4, 6, 9 | 3bitri 262 |
. . . . . . . . 9
Ins2 Ins2
S
|
11 | 8 | oqelins4 5794 |
. . . . . . . . . 10
Ins4 Ins2 Ins2
S Ins4 SI3 Ins3 Disj Cup 1c
Ins2 Ins2 S Ins4 SI3 Ins3 Disj Cup 1c |
12 | | elin 3219 |
. . . . . . . . . . . . 13
Ins2 Ins2 S Ins4
SI3 Ins3 Disj Cup Ins2 Ins2 S
Ins4 SI3 Ins3 Disj Cup |
13 | | snex 4111 |
. . . . . . . . . . . . . . . 16
|
14 | 13 | otelins2 5791 |
. . . . . . . . . . . . . . 15
Ins2 Ins2 S Ins2 S |
15 | 3 | otelins2 5791 |
. . . . . . . . . . . . . . 15
Ins2 S
S |
16 | | vex 2862 |
. . . . . . . . . . . . . . . 16
|
17 | 16, 5 | opelssetsn 4760 |
. . . . . . . . . . . . . . 15
S |
18 | 14, 15, 17 | 3bitri 262 |
. . . . . . . . . . . . . 14
Ins2 Ins2 S |
19 | 5 | oqelins4 5794 |
. . . . . . . . . . . . . . 15
Ins4 SI3
Ins3 Disj Cup
SI3 Ins3 Disj Cup |
20 | | vex 2862 |
. . . . . . . . . . . . . . . 16
|
21 | 16, 7, 20 | otsnelsi3 5805 |
. . . . . . . . . . . . . . 15
SI3 Ins3 Disj Cup
Ins3 Disj Cup |
22 | | elin 3219 |
. . . . . . . . . . . . . . . 16
Ins3 Disj Cup Ins3 Disj
Cup |
23 | 20 | otelins3 5792 |
. . . . . . . . . . . . . . . . . 18
Ins3
Disj Disj |
24 | | df-br 4640 |
. . . . . . . . . . . . . . . . . 18
Disj Disj |
25 | 16, 7 | brdisj 5822 |
. . . . . . . . . . . . . . . . . 18
Disj |
26 | 23, 24, 25 | 3bitr2i 264 |
. . . . . . . . . . . . . . . . 17
Ins3
Disj
|
27 | | trtxp 5781 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
28 | 27 | anbi2i 675 |
. . . . . . . . . . . . . . . . . . . . . 22
|
29 | | trtxp 5781 |
. . . . . . . . . . . . . . . . . . . . . 22
|
30 | | anass 630 |
. . . . . . . . . . . . . . . . . . . . . 22
|
31 | 28, 29, 30 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . 21
|
32 | | brco 4883 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
33 | 16 | br1st 4858 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
34 | 33 | anbi2i 675 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
35 | | 19.42v 1905 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
36 | 34, 35 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
37 | 36 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
38 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
39 | | exancom 1586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
40 | 16, 8 | opex 4588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
41 | | breq2 4643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
42 | 40, 41 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
43 | 39, 42 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
44 | 43 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
45 | 38, 44 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
46 | 32, 37, 45 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
47 | 46 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
48 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
49 | 40 | br1st 4858 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
50 | | breq1 4642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
51 | 40, 20 | brco1st 5777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
52 | 16, 8 | opbr2nd 5502 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
53 | 51, 52 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
54 | 50, 53 | syl6bb 252 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
55 | 54 | exlimiv 1634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
56 | 49, 55 | sylbi 187 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
57 | 56 | pm5.32i 618 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
58 | 57 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
59 | | exancom 1586 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
60 | 58, 59 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
61 | 47, 48, 60 | 3bitr2i 264 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
62 | | opeq2 4579 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
63 | 62 | breq2d 4651 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
64 | 7, 63 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
65 | 61, 64 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . 22
|
66 | 65 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . 21
|
67 | 16, 7 | opex 4588 |
. . . . . . . . . . . . . . . . . . . . . 22
|
68 | 67, 20 | op1st2nd 5790 |
. . . . . . . . . . . . . . . . . . . . 21
|
69 | 31, 66, 68 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . 20
|
70 | 69 | rexbii 2639 |
. . . . . . . . . . . . . . . . . . 19
Cup
Cup |
71 | | elima 4754 |
. . . . . . . . . . . . . . . . . . 19
Cup Cup |
72 | | risset 2661 |
. . . . . . . . . . . . . . . . . . 19
Cup Cup |
73 | 70, 71, 72 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . 18
Cup Cup |
74 | | df-br 4640 |
. . . . . . . . . . . . . . . . . 18
Cup
Cup |
75 | 16, 7 | brcup 5815 |
. . . . . . . . . . . . . . . . . 18
Cup
|
76 | 73, 74, 75 | 3bitr2i 264 |
. . . . . . . . . . . . . . . . 17
Cup |
77 | 26, 76 | anbi12i 678 |
. . . . . . . . . . . . . . . 16
Ins3
Disj
Cup |
78 | 22, 77 | bitri 240 |
. . . . . . . . . . . . . . 15
Ins3 Disj Cup |
79 | 19, 21, 78 | 3bitri 262 |
. . . . . . . . . . . . . 14
Ins4 SI3
Ins3 Disj Cup
|
80 | 18, 79 | anbi12i 678 |
. . . . . . . . . . . . 13
Ins2
Ins2 S Ins4 SI3
Ins3 Disj Cup
|
81 | 12, 80 | bitri 240 |
. . . . . . . . . . . 12
Ins2 Ins2 S Ins4
SI3 Ins3 Disj Cup
|
82 | 81 | exbii 1582 |
. . . . . . . . . . 11
Ins2 Ins2 S Ins4
SI3 Ins3 Disj Cup
|
83 | | elima1c 4947 |
. . . . . . . . . . 11
Ins2 Ins2 S Ins4
SI3 Ins3 Disj Cup 1c Ins2 Ins2 S Ins4
SI3 Ins3 Disj Cup |
84 | | df-rex 2620 |
. . . . . . . . . . 11
|
85 | 82, 83, 84 | 3bitr4i 268 |
. . . . . . . . . 10
Ins2 Ins2 S Ins4
SI3 Ins3 Disj Cup 1c |
86 | 11, 85 | bitri 240 |
. . . . . . . . 9
Ins4 Ins2 Ins2
S Ins4 SI3 Ins3 Disj Cup 1c |
87 | 10, 86 | anbi12i 678 |
. . . . . . . 8
Ins2 Ins2
S Ins4 Ins2 Ins2 S Ins4 SI3 Ins3 Disj Cup 1c
|
88 | 2, 87 | bitri 240 |
. . . . . . 7
Ins2 Ins2 S Ins4 Ins2 Ins2
S Ins4 SI3 Ins3 Disj Cup 1c
|
89 | 88 | exbii 1582 |
. . . . . 6
Ins2 Ins2 S Ins4
Ins2 Ins2 S Ins4
SI3 Ins3 Disj Cup 1c
|
90 | | elima1c 4947 |
. . . . . 6
Ins2 Ins2 S Ins4 Ins2 Ins2
S Ins4 SI3 Ins3 Disj Cup 1c1c
Ins2 Ins2 S Ins4 Ins2 Ins2
S Ins4 SI3 Ins3 Disj Cup 1c |
91 | | df-rex 2620 |
. . . . . 6
|
92 | 89, 90, 91 | 3bitr4i 268 |
. . . . 5
Ins2 Ins2 S Ins4 Ins2 Ins2
S Ins4 SI3 Ins3 Disj Cup 1c1c |
93 | | eladdc 4398 |
. . . . . 6
|
94 | | rexcom 2772 |
. . . . . 6
|
95 | 93, 94 | bitri 240 |
. . . . 5
|
96 | 92, 95 | bitr4i 243 |
. . . 4
Ins2 Ins2 S Ins4 Ins2 Ins2
S Ins4 SI3 Ins3 Disj Cup 1c1c |
97 | 96 | releqmpt2 5809 |
. . 3
Ins2 S Ins3 Ins2 Ins2 S Ins4 Ins2 Ins2
S Ins4 SI3 Ins3 Disj Cup 1c1c1c
|
98 | 1, 97 | eqtr4i 2376 |
. 2
AddC Ins2 S
Ins3 Ins2 Ins2 S Ins4 Ins2 Ins2
S Ins4 SI3 Ins3 Disj Cup 1c1c1c |
99 | | vvex 4109 |
. . 3
|
100 | | ssetex 4744 |
. . . . . . 7
S |
101 | 100 | ins2ex 5797 |
. . . . . 6
Ins2 S |
102 | 101 | ins2ex 5797 |
. . . . 5
Ins2 Ins2 S |
103 | | disjex 5823 |
. . . . . . . . . . . 12
Disj |
104 | 103 | ins3ex 5798 |
. . . . . . . . . . 11
Ins3 Disj |
105 | | 1stex 4739 |
. . . . . . . . . . . . . 14
|
106 | 105, 105 | coex 4750 |
. . . . . . . . . . . . 13
|
107 | | 2ndex 5112 |
. . . . . . . . . . . . . . 15
|
108 | 107, 105 | coex 4750 |
. . . . . . . . . . . . . 14
|
109 | 108, 107 | txpex 5785 |
. . . . . . . . . . . . 13
|
110 | 106, 109 | txpex 5785 |
. . . . . . . . . . . 12
|
111 | | cupex 5816 |
. . . . . . . . . . . 12
Cup |
112 | 110, 111 | imaex 4747 |
. . . . . . . . . . 11
Cup |
113 | 104, 112 | inex 4105 |
. . . . . . . . . 10
Ins3 Disj Cup |
114 | 113 | si3ex 5806 |
. . . . . . . . 9
SI3 Ins3 Disj Cup |
115 | 114 | ins4ex 5799 |
. . . . . . . 8
Ins4 SI3
Ins3 Disj Cup |
116 | 102, 115 | inex 4105 |
. . . . . . 7
Ins2 Ins2 S Ins4 SI3 Ins3 Disj Cup |
117 | | 1cex 4142 |
. . . . . . 7
1c
|
118 | 116, 117 | imaex 4747 |
. . . . . 6
Ins2 Ins2 S Ins4
SI3 Ins3 Disj Cup 1c |
119 | 118 | ins4ex 5799 |
. . . . 5
Ins4 Ins2 Ins2 S Ins4 SI3 Ins3 Disj Cup 1c |
120 | 102, 119 | inex 4105 |
. . . 4
Ins2 Ins2 S Ins4 Ins2 Ins2
S Ins4 SI3 Ins3 Disj Cup 1c |
121 | 120, 117 | imaex 4747 |
. . 3
Ins2 Ins2 S Ins4
Ins2 Ins2 S Ins4
SI3 Ins3 Disj Cup 1c1c |
122 | 99, 99, 121 | mpt2exlem 5811 |
. 2
Ins2 S Ins3 Ins2 Ins2 S Ins4 Ins2 Ins2
S Ins4 SI3 Ins3 Disj Cup 1c1c1c |
123 | 98, 122 | eqeltri 2423 |
1
AddC |