Step | Hyp | Ref
| Expression |
1 | | unab 3521 |
. . 3
c We NC
NC Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c
c We NC NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
2 | | elima3 4756 |
. . . . . 6
1c AddC ⋃1 ∼ SI S SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c1 1 1 NC
⋃1
∼ SI S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c1 1 1 NC 1c AddC |
3 | | vex 2862 |
. . . . . . . . . . 11
|
4 | 3 | eluni1 4173 |
. . . . . . . . . 10
⋃1 ∼ SI S
SI ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c1 1 1 NC ∼ SI S
SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c1 1 1 NC |
5 | | snex 4111 |
. . . . . . . . . . 11
|
6 | 5 | elcompl 3225 |
. . . . . . . . . 10
∼
SI S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c1 1 1 NC
SI S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c1 1 1 NC |
7 | | elimapw13 4946 |
. . . . . . . . . . . 12
SI S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c1 1 1 NC NC SI S
SI ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c |
8 | | spacval 6280 |
. . . . . . . . . . . . . . . . . 18
NC Spac
Clos1 NC NC 2c ↑c
|
9 | 8 | nceqd 6110 |
. . . . . . . . . . . . . . . . 17
NC Nc Spac Nc Clos1 NC NC 2c ↑c
|
10 | 9 | eqeq1d 2361 |
. . . . . . . . . . . . . . . 16
NC Nc Spac
Nc Clos1 NC NC 2c ↑c
|
11 | | tccl 6160 |
. . . . . . . . . . . . . . . . . . . 20
NC Tc NC |
12 | | spacval 6280 |
. . . . . . . . . . . . . . . . . . . 20
Tc
NC Spac Tc
Clos1 Tc
NC NC 2c ↑c
|
13 | 11, 12 | syl 15 |
. . . . . . . . . . . . . . . . . . 19
NC Spac Tc
Clos1 Tc
NC NC 2c ↑c
|
14 | 13 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . 18
NC Spac Tc Fin Clos1
Tc
NC NC 2c ↑c
Fin |
15 | 13 | nceqd 6110 |
. . . . . . . . . . . . . . . . . . . 20
NC Nc Spac Tc Nc Clos1
Tc
NC NC 2c ↑c
|
16 | 15 | eqeq1d 2361 |
. . . . . . . . . . . . . . . . . . 19
NC Nc Spac Tc
Tc 1c Nc Clos1
Tc
NC NC 2c ↑c
Tc 1c |
17 | 15 | eqeq1d 2361 |
. . . . . . . . . . . . . . . . . . 19
NC Nc Spac Tc
Tc 2c Nc Clos1
Tc
NC NC 2c ↑c
Tc 2c |
18 | 16, 17 | orbi12d 690 |
. . . . . . . . . . . . . . . . . 18
NC Nc Spac Tc
Tc 1c Nc Spac Tc
Tc 2c Nc Clos1 Tc NC NC 2c ↑c
Tc 1c Nc
Clos1 Tc
NC NC 2c ↑c
Tc 2c |
19 | 14, 18 | anbi12d 691 |
. . . . . . . . . . . . . . . . 17
NC Spac Tc Fin Nc Spac Tc
Tc 1c Nc Spac Tc
Tc 2c Clos1
Tc
NC NC 2c ↑c
Fin Nc Clos1 Tc NC NC 2c ↑c
Tc 1c Nc
Clos1 Tc
NC NC 2c ↑c
Tc 2c |
20 | 19 | notbid 285 |
. . . . . . . . . . . . . . . 16
NC Spac
Tc
Fin Nc Spac Tc
Tc 1c Nc Spac Tc
Tc 2c Clos1 Tc
NC NC 2c ↑c
Fin Nc Clos1 Tc NC NC 2c ↑c
Tc 1c Nc
Clos1 Tc
NC NC 2c ↑c
Tc 2c |
21 | 10, 20 | anbi12d 691 |
. . . . . . . . . . . . . . 15
NC Nc Spac
Spac Tc Fin Nc Spac Tc
Tc 1c Nc Spac Tc
Tc 2c Nc Clos1
NC NC 2c ↑c
Clos1 Tc
NC NC 2c ↑c
Fin Nc Clos1 Tc NC NC 2c ↑c
Tc 1c Nc
Clos1 Tc
NC NC 2c ↑c
Tc 2c |
22 | | eldif 3221 |
. . . . . . . . . . . . . . . 16
SI
S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c SI S SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c |
23 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . 20
|
24 | 23, 3 | opsnelsi 5774 |
. . . . . . . . . . . . . . . . . . 19
SI S
SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC |
25 | | opelcnv 4893 |
. . . . . . . . . . . . . . . . . . 19
S SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC S
SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC |
26 | | opelres 4950 |
. . . . . . . . . . . . . . . . . . . 20
S SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC S
SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC |
27 | | opelcnv 4893 |
. . . . . . . . . . . . . . . . . . . . . 22
S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c |
28 | | opelco 4884 |
. . . . . . . . . . . . . . . . . . . . . . 23
S
SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S |
29 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
30 | 29 | brsnsi1 5775 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c
∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c |
31 | 30 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S |
32 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S
∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S |
33 | 31, 32 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S |
34 | 33 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . 24
SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S |
35 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . . 24
∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S |
36 | 34, 35 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . 23
SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S |
37 | | anass 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S |
38 | 37 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S |
39 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
40 | | breq1 4642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
S S |
41 | 40 | anbi2d 684 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S |
42 | 39, 41 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S |
43 | | brcnv 4892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c |
44 | | df-br 4640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c |
45 | | spacvallem1 6279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
NC NC 2c ↑c
|
46 | 45, 29 | nchoicelem10 6296 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c
Clos1
NC NC 2c ↑c
|
47 | 43, 44, 46 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c Clos1
NC NC 2c ↑c
|
48 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
49 | 48, 3 | brssetsn 4759 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
S |
50 | 47, 49 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S
Clos1 NC NC 2c ↑c
|
51 | 38, 42, 50 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . 24
∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S Clos1
NC NC 2c ↑c
|
52 | 51 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . 23
∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S Clos1 NC NC 2c ↑c
|
53 | 28, 36, 52 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . 22
S
SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c
Clos1 NC NC 2c ↑c
|
54 | 29, 45 | clos1ex 5876 |
. . . . . . . . . . . . . . . . . . . . . . 23
Clos1 NC NC 2c ↑c
|
55 | | eleq1 2413 |
. . . . . . . . . . . . . . . . . . . . . . 23
Clos1 NC NC
2c
↑c Clos1 NC NC
2c
↑c
|
56 | 54, 55 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . 22
Clos1
NC NC 2c ↑c
Clos1 NC NC 2c ↑c
|
57 | 27, 53, 56 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . 21
S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c Clos1 NC NC 2c ↑c
|
58 | 57 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . 20
S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC Clos1 NC NC
2c
↑c
NC |
59 | | ancom 437 |
. . . . . . . . . . . . . . . . . . . 20
Clos1
NC NC 2c ↑c
NC NC
Clos1
NC NC 2c ↑c
|
60 | 26, 58, 59 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . 19
S SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC NC
Clos1
NC NC 2c ↑c
|
61 | 24, 25, 60 | 3bitri 262 |
. . . . . . . . . . . . . . . . . 18
SI S
SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC NC
Clos1
NC NC 2c ↑c
|
62 | | eqcom 2355 |
. . . . . . . . . . . . . . . . . . 19
Nc Clos1 NC NC 2c ↑c
Nc Clos1 NC NC 2c ↑c
|
63 | 54 | eqnc2 6129 |
. . . . . . . . . . . . . . . . . . 19
Nc Clos1
NC NC 2c ↑c
NC Clos1
NC NC 2c ↑c
|
64 | 62, 63 | bitri 240 |
. . . . . . . . . . . . . . . . . 18
Nc Clos1 NC NC 2c ↑c
NC Clos1 NC NC
2c
↑c
|
65 | 61, 64 | bitr4i 243 |
. . . . . . . . . . . . . . . . 17
SI S
SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC Nc Clos1
NC NC 2c ↑c
|
66 | | elimapw11c 4948 |
. . . . . . . . . . . . . . . . . . 19
SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC |
67 | | oteltxp 5782 |
. . . . . . . . . . . . . . . . . . . . 21
SI SI
TcFn TcFn
AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC |
68 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
69 | 68, 23 | opsnelsi 5774 |
. . . . . . . . . . . . . . . . . . . . . . 23
SI SI TcFn SI TcFn |
70 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
71 | 70, 29 | opsnelsi 5774 |
. . . . . . . . . . . . . . . . . . . . . . . 24
SI TcFn
TcFn |
72 | | df-br 4640 |
. . . . . . . . . . . . . . . . . . . . . . . 24
TcFn TcFn |
73 | | brcnv 4892 |
. . . . . . . . . . . . . . . . . . . . . . . 24
TcFn TcFn |
74 | 71, 72, 73 | 3bitr2i 264 |
. . . . . . . . . . . . . . . . . . . . . . 23
SI TcFn TcFn |
75 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
76 | 75 | brtcfn 6245 |
. . . . . . . . . . . . . . . . . . . . . . 23
TcFn Tc |
77 | 69, 74, 76 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . 22
SI SI TcFn Tc |
78 | | opelco 4884 |
. . . . . . . . . . . . . . . . . . . . . . 23
TcFn AddC 1c AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC S
SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC TcFn
AddC 1c
AddC
2c Nn |
79 | | brcnv 4892 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
S SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC S SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC |
80 | | brres 4949 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
S
SI ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC |
81 | | brcnv 4892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
S SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S
SI ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c |
82 | | brco 4883 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
S
SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S |
83 | 68 | brsnsi1 5775 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c
∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c |
84 | 83 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S |
85 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S
∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S |
86 | 84, 85 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S |
87 | 86 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S |
88 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S |
89 | | anass 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S |
90 | 89 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S |
91 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
92 | | breq1 4642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
S S |
93 | 92 | anbi2d 684 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S |
94 | 91, 93 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S |
95 | | brcnv 4892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c |
96 | | df-br 4640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c |
97 | 45, 68 | nchoicelem10 6296 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c
Clos1
NC NC 2c ↑c
|
98 | 95, 96, 97 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c Clos1
NC NC 2c ↑c
|
99 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
100 | 99, 48 | brssetsn 4759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
S |
101 | 98, 100 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S
Clos1 NC NC 2c ↑c
|
102 | 90, 94, 101 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S Clos1
NC NC 2c ↑c
|
103 | 102 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S Clos1 NC NC 2c ↑c
|
104 | 87, 88, 103 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S Clos1 NC NC
2c
↑c |
105 | | df-clel 2349 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Clos1
NC NC 2c ↑c
Clos1 NC NC
2c
↑c |
106 | 104, 105 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c S Clos1
NC NC 2c ↑c
|
107 | 81, 82, 106 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
S SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c Clos1 NC NC 2c ↑c
|
108 | 107 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
S
SI ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC Clos1 NC NC
2c
↑c
NC |
109 | | ancom 437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Clos1
NC NC 2c ↑c
NC NC
Clos1
NC NC 2c ↑c
|
110 | 80, 108, 109 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
S
SI ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC NC
Clos1
NC NC 2c ↑c
|
111 | 68, 45 | clos1ex 5876 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Clos1 NC NC 2c ↑c
|
112 | 111 | eqnc2 6129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Nc Clos1
NC NC 2c ↑c
NC Clos1
NC NC 2c ↑c
|
113 | 110, 112 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
S
SI ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC Nc Clos1 NC NC 2c ↑c
|
114 | 79, 113 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
S SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC Nc Clos1 NC NC 2c ↑c
|
115 | | brres 4949 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
TcFn AddC 1c AddC
2c Nn TcFn AddC 1c AddC
2c Nn |
116 | | brco 4883 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
TcFn
AddC 1c
AddC
2c AddC 1c AddC
2c TcFn |
117 | | brcnv 4892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
AddC 1c AddC
2c AddC 1c
AddC
2c |
118 | | brun 4692 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
AddC 1c AddC
2c AddC 1c AddC 2c |
119 | | brco 4883 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
AddC 1c 1c AddC |
120 | | brcnv 4892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
1c
1c |
121 | | brres 4949 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
1c
1c |
122 | | eliniseg 5020 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
1c 1c |
123 | 122 | anbi2i 675 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
1c
1c |
124 | 121, 123 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
1c
1c |
125 | | 1cex 4142 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
1c
|
126 | 99, 125 | op1st2nd 5790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
1c
1c |
127 | 120, 124,
126 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
1c
1c |
128 | 127 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
1c AddC
1c AddC |
129 | 128 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
1c
AddC
1c AddC |
130 | 99, 125 | opex 4588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
1c |
131 | | breq1 4642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
1c AddC 1c AddC
|
132 | 130, 131 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
1c AddC 1c AddC |
133 | 119, 129,
132 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
AddC 1c 1c AddC |
134 | 99, 125 | braddcfn 5826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
1c AddC
1c
|
135 | | eqcom 2355 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
1c
1c |
136 | 133, 134,
135 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
AddC 1c
1c |
137 | | brco 4883 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
AddC 2c 2c AddC |
138 | | brcnv 4892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
2c
2c |
139 | | brres 4949 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
2c
2c |
140 | | eliniseg 5020 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
2c 2c |
141 | 140 | anbi2i 675 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
2c
2c |
142 | 139, 141 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
2c
2c |
143 | | 2nc 6168 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
2c
NC |
144 | 143 | elexi 2868 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
2c
|
145 | 99, 144 | op1st2nd 5790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
2c
2c |
146 | 138, 142,
145 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
2c
2c |
147 | 146 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
2c AddC
2c AddC |
148 | 147 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
2c
AddC
2c AddC |
149 | 99, 144 | opex 4588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
2c |
150 | | breq1 4642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
2c AddC 2c AddC
|
151 | 149, 150 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
2c AddC 2c AddC |
152 | 137, 148,
151 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
AddC 2c 2c AddC |
153 | 99, 144 | braddcfn 5826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
2c AddC
2c
|
154 | | eqcom 2355 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
2c
2c |
155 | 152, 153,
154 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
AddC 2c
2c |
156 | 136, 155 | orbi12i 507 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
AddC 1c AddC 2c
1c
2c |
157 | 117, 118,
156 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
AddC 1c AddC
2c 1c
2c |
158 | | brcnv 4892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
TcFn TcFn |
159 | 3 | brtcfn 6245 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
TcFn Tc |
160 | 158, 159 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
TcFn
Tc |
161 | 157, 160 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
AddC
1c AddC 2c TcFn
1c
2c Tc |
162 | | ancom 437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
1c
2c Tc Tc
1c
2c |
163 | 161, 162 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
AddC
1c AddC 2c TcFn
Tc
1c
2c |
164 | 163 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
AddC 1c
AddC
2c TcFn Tc
1c
2c |
165 | | tcex 6157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Tc
|
166 | | addceq1 4383 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Tc
1c
Tc 1c |
167 | 166 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Tc
1c
Tc 1c |
168 | | addceq1 4383 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Tc
2c
Tc 2c |
169 | 168 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Tc
2c
Tc 2c |
170 | 167, 169 | orbi12d 690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Tc
1c
2c Tc 1c Tc 2c |
171 | 165, 170 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Tc
1c
2c Tc 1c Tc 2c |
172 | 116, 164,
171 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
TcFn
AddC 1c
AddC
2c Tc 1c
Tc 2c |
173 | 172 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
TcFn AddC 1c AddC
2c Nn Tc 1c Tc 2c
Nn |
174 | | ancom 437 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Tc 1c
Tc 2c Nn Nn Tc 1c Tc 2c |
175 | 115, 173,
174 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
TcFn AddC 1c AddC
2c Nn
Nn Tc 1c Tc 2c |
176 | 114, 175 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . 24
S
SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC TcFn
AddC 1c
AddC
2c Nn Nc Clos1 NC NC 2c ↑c
Nn Tc 1c
Tc 2c |
177 | 176 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . 23
S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC TcFn
AddC 1c
AddC
2c Nn Nc Clos1
NC NC 2c ↑c
Nn Tc 1c
Tc 2c |
178 | | ncex 6117 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Nc Clos1 NC NC 2c ↑c
|
179 | | eleq1 2413 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Nc Clos1
NC NC 2c ↑c
Nn Nc Clos1 NC NC 2c ↑c
Nn |
180 | | finnc 6242 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Clos1
NC NC 2c ↑c
Fin Nc Clos1 NC NC 2c ↑c
Nn |
181 | 179, 180 | syl6bbr 254 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Nc Clos1
NC NC 2c ↑c
Nn Clos1
NC NC 2c ↑c
Fin |
182 | | eqeq1 2359 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Nc Clos1
NC NC 2c ↑c
Tc 1c Nc Clos1
NC NC 2c ↑c
Tc 1c |
183 | | eqeq1 2359 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Nc Clos1
NC NC 2c ↑c
Tc 2c Nc Clos1
NC NC 2c ↑c
Tc 2c |
184 | 182, 183 | orbi12d 690 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Nc Clos1
NC NC 2c ↑c
Tc 1c Tc 2c
Nc Clos1 NC NC 2c ↑c
Tc 1c Nc
Clos1
NC NC 2c ↑c
Tc 2c |
185 | 181, 184 | anbi12d 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Nc Clos1
NC NC 2c ↑c
Nn Tc 1c Tc 2c
Clos1
NC NC 2c ↑c
Fin Nc Clos1 NC NC 2c ↑c
Tc 1c Nc
Clos1
NC NC 2c ↑c
Tc 2c |
186 | 178, 185 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . . 23
Nc Clos1 NC NC 2c ↑c
Nn Tc 1c
Tc 2c Clos1 NC NC
2c
↑c
Fin
Nc Clos1
NC NC 2c ↑c
Tc 1c Nc
Clos1
NC NC 2c ↑c
Tc 2c |
187 | 78, 177, 186 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . 22
TcFn AddC 1c AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC Clos1
NC NC 2c ↑c
Fin Nc Clos1 NC NC 2c ↑c
Tc 1c Nc
Clos1
NC NC 2c ↑c
Tc 2c |
188 | 77, 187 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . 21
SI
SI TcFn TcFn AddC 1c AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC Tc Clos1 NC NC
2c
↑c
Fin
Nc Clos1
NC NC 2c ↑c
Tc 1c Nc
Clos1
NC NC 2c ↑c
Tc 2c |
189 | 67, 188 | bitri 240 |
. . . . . . . . . . . . . . . . . . . 20
SI SI
TcFn TcFn
AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC Tc Clos1 NC NC
2c
↑c
Fin
Nc Clos1
NC NC 2c ↑c
Tc 1c Nc
Clos1
NC NC 2c ↑c
Tc 2c |
190 | 189 | exbii 1582 |
. . . . . . . . . . . . . . . . . . 19
SI SI
TcFn TcFn
AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC
Tc Clos1 NC NC 2c ↑c
Fin Nc Clos1 NC NC 2c ↑c
Tc 1c Nc
Clos1
NC NC 2c ↑c
Tc 2c |
191 | | tcex 6157 |
. . . . . . . . . . . . . . . . . . . 20
Tc
|
192 | | sneq 3744 |
. . . . . . . . . . . . . . . . . . . . . . 23
Tc Tc |
193 | | clos1eq1 5874 |
. . . . . . . . . . . . . . . . . . . . . . 23
Tc Clos1 NC NC 2c ↑c
Clos1 Tc
NC NC 2c ↑c
|
194 | 192, 193 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . 22
Tc Clos1 NC NC 2c ↑c
Clos1 Tc
NC NC 2c ↑c
|
195 | 194 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . 21
Tc Clos1 NC NC
2c
↑c
Fin Clos1 Tc
NC NC 2c ↑c
Fin |
196 | 194 | nceqd 6110 |
. . . . . . . . . . . . . . . . . . . . . . 23
Tc Nc
Clos1
NC NC 2c ↑c
Nc Clos1 Tc NC NC 2c ↑c
|
197 | 196 | eqeq1d 2361 |
. . . . . . . . . . . . . . . . . . . . . 22
Tc Nc Clos1
NC NC 2c ↑c
Tc 1c Nc Clos1 Tc
NC NC 2c ↑c
Tc 1c |
198 | 196 | eqeq1d 2361 |
. . . . . . . . . . . . . . . . . . . . . 22
Tc Nc Clos1
NC NC 2c ↑c
Tc 2c Nc Clos1 Tc
NC NC 2c ↑c
Tc 2c |
199 | 197, 198 | orbi12d 690 |
. . . . . . . . . . . . . . . . . . . . 21
Tc Nc Clos1 NC NC 2c ↑c
Tc 1c Nc
Clos1
NC NC 2c ↑c
Tc 2c Nc Clos1
Tc
NC NC 2c ↑c
Tc 1c Nc
Clos1 Tc
NC NC 2c ↑c
Tc 2c |
200 | 195, 199 | anbi12d 691 |
. . . . . . . . . . . . . . . . . . . 20
Tc Clos1 NC NC 2c ↑c
Fin Nc Clos1 NC NC 2c ↑c
Tc 1c Nc
Clos1
NC NC 2c ↑c
Tc 2c
Clos1 Tc
NC NC 2c ↑c
Fin Nc Clos1 Tc NC NC 2c ↑c
Tc 1c Nc
Clos1 Tc
NC NC 2c ↑c
Tc 2c |
201 | 191, 200 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . 19
Tc Clos1 NC NC 2c ↑c
Fin Nc Clos1 NC NC 2c ↑c
Tc 1c Nc
Clos1
NC NC 2c ↑c
Tc 2c Clos1
Tc
NC NC 2c ↑c
Fin Nc Clos1 Tc NC NC 2c ↑c
Tc 1c Nc
Clos1 Tc
NC NC 2c ↑c
Tc 2c |
202 | 66, 190, 201 | 3bitri 262 |
. . . . . . . . . . . . . . . . . 18
SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c Clos1 Tc
NC NC 2c ↑c
Fin Nc Clos1 Tc NC NC 2c ↑c
Tc 1c Nc
Clos1 Tc
NC NC 2c ↑c
Tc 2c |
203 | 202 | notbii 287 |
. . . . . . . . . . . . . . . . 17
SI SI
TcFn TcFn
AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c Clos1 Tc
NC NC 2c ↑c
Fin Nc Clos1 Tc NC NC 2c ↑c
Tc 1c Nc
Clos1 Tc
NC NC 2c ↑c
Tc 2c |
204 | 65, 203 | anbi12i 678 |
. . . . . . . . . . . . . . . 16
SI
S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c Nc Clos1 NC NC 2c ↑c
Clos1 Tc
NC NC 2c ↑c
Fin Nc Clos1 Tc NC NC 2c ↑c
Tc 1c Nc
Clos1 Tc
NC NC 2c ↑c
Tc 2c |
205 | 22, 204 | bitri 240 |
. . . . . . . . . . . . . . 15
SI
S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c Nc Clos1 NC NC 2c ↑c
Clos1 Tc
NC NC 2c ↑c
Fin Nc Clos1 Tc NC NC 2c ↑c
Tc 1c Nc
Clos1 Tc
NC NC 2c ↑c
Tc 2c |
206 | 21, 205 | syl6rbbr 255 |
. . . . . . . . . . . . . 14
NC SI S
SI ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c Nc Spac
Spac Tc Fin Nc Spac Tc
Tc 1c Nc Spac Tc
Tc 2c |
207 | | tceq 6158 |
. . . . . . . . . . . . . . . . . . . 20
Nc Spac
Tc Nc Spac
Tc |
208 | 207 | addceq1d 4389 |
. . . . . . . . . . . . . . . . . . 19
Nc Spac
Tc Nc Spac
1c
Tc 1c |
209 | 208 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . 18
Nc Spac
Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc 1c |
210 | 207 | addceq1d 4389 |
. . . . . . . . . . . . . . . . . . 19
Nc Spac
Tc Nc Spac
2c
Tc 2c |
211 | 210 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . 18
Nc Spac
Nc Spac Tc
Tc Nc Spac
2c
Nc Spac Tc
Tc 2c |
212 | 209, 211 | orbi12d 690 |
. . . . . . . . . . . . . . . . 17
Nc Spac
Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c Nc Spac Tc
Tc 1c Nc Spac Tc
Tc 2c |
213 | 212 | anbi2d 684 |
. . . . . . . . . . . . . . . 16
Nc Spac
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c Spac
Tc
Fin Nc Spac Tc
Tc 1c Nc Spac Tc
Tc 2c |
214 | 213 | notbid 285 |
. . . . . . . . . . . . . . 15
Nc Spac
Spac
Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c Spac Tc
Fin Nc Spac Tc
Tc 1c Nc Spac Tc
Tc 2c |
215 | 214 | pm5.32i 618 |
. . . . . . . . . . . . . 14
Nc Spac Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c Nc Spac
Spac Tc Fin Nc Spac Tc
Tc 1c Nc Spac Tc
Tc 2c |
216 | 206, 215 | syl6bbr 254 |
. . . . . . . . . . . . 13
NC SI S
SI ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c Nc Spac
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
217 | 216 | rexbiia 2647 |
. . . . . . . . . . . 12
NC SI S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c NC Nc Spac
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
218 | | rexanali 2660 |
. . . . . . . . . . . 12
NC Nc Spac
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c NC Nc Spac
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
219 | 7, 217, 218 | 3bitrri 263 |
. . . . . . . . . . 11
NC Nc Spac
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c SI S
SI ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c1 1 1 NC |
220 | 219 | con1bii 321 |
. . . . . . . . . 10
SI S
SI ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c1 1 1 NC NC Nc Spac
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
221 | 4, 6, 220 | 3bitri 262 |
. . . . . . . . 9
⋃1 ∼ SI S
SI ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c1 1 1 NC NC Nc Spac
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
222 | | opelco 4884 |
. . . . . . . . . . 11
1c AddC AddC 1c |
223 | | brcnv 4892 |
. . . . . . . . . . . . . 14
AddC AddC |
224 | | brres 4949 |
. . . . . . . . . . . . . . 15
1c
1c |
225 | | eliniseg 5020 |
. . . . . . . . . . . . . . . . 17
1c 1c |
226 | 225 | anbi2i 675 |
. . . . . . . . . . . . . . . 16
1c
1c |
227 | | ancom 437 |
. . . . . . . . . . . . . . . 16
1c 1c |
228 | 226, 227 | bitri 240 |
. . . . . . . . . . . . . . 15
1c 1c |
229 | 125, 99 | op1st2nd 5790 |
. . . . . . . . . . . . . . 15
1c 1c |
230 | 224, 228,
229 | 3bitri 262 |
. . . . . . . . . . . . . 14
1c
1c |
231 | 223, 230 | anbi12i 678 |
. . . . . . . . . . . . 13
AddC 1c AddC 1c |
232 | | ancom 437 |
. . . . . . . . . . . . 13
AddC
1c 1c AddC |
233 | 231, 232 | bitri 240 |
. . . . . . . . . . . 12
AddC 1c 1c AddC |
234 | 233 | exbii 1582 |
. . . . . . . . . . 11
AddC 1c 1c AddC |
235 | 125, 99 | opex 4588 |
. . . . . . . . . . . 12
1c |
236 | | breq1 4642 |
. . . . . . . . . . . 12
1c
AddC 1c
AddC |
237 | 235, 236 | ceqsexv 2894 |
. . . . . . . . . . 11
1c AddC 1c AddC |
238 | 222, 234,
237 | 3bitri 262 |
. . . . . . . . . 10
1c AddC 1c AddC |
239 | 125, 99 | braddcfn 5826 |
. . . . . . . . . 10
1c AddC 1c |
240 | | eqcom 2355 |
. . . . . . . . . 10
1c 1c |
241 | 238, 239,
240 | 3bitri 262 |
. . . . . . . . 9
1c AddC 1c |
242 | 221, 241 | anbi12i 678 |
. . . . . . . 8
⋃1 ∼ SI S
SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c1 1 1 NC 1c AddC
NC Nc Spac
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c
1c |
243 | | ancom 437 |
. . . . . . . 8
NC Nc Spac
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c
1c 1c
NC Nc Spac
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
244 | 242, 243 | bitri 240 |
. . . . . . 7
⋃1 ∼ SI S
SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c1 1 1 NC 1c AddC 1c
NC Nc Spac
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
245 | 244 | exbii 1582 |
. . . . . 6
⋃1 ∼
SI S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c1 1 1 NC 1c AddC
1c
NC Nc Spac Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
246 | 125, 99 | addcex 4394 |
. . . . . . 7
1c
|
247 | | eqeq2 2362 |
. . . . . . . . 9
1c Nc Spac Nc Spac 1c |
248 | 247 | imbi1d 308 |
. . . . . . . 8
1c Nc Spac
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
249 | 248 | ralbidv 2634 |
. . . . . . 7
1c
NC Nc Spac
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c
NC Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
250 | 246, 249 | ceqsexv 2894 |
. . . . . 6
1c
NC Nc Spac
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
251 | 2, 245, 250 | 3bitri 262 |
. . . . 5
1c AddC ⋃1 ∼ SI S SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c1 1 1 NC NC Nc Spac 1c Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
252 | 251 | abbi2i 2464 |
. . . 4
1c AddC ⋃1 ∼ SI S
SI ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c1 1 1 NC
NC Nc Spac 1c Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
253 | 252 | uneq2i 3415 |
. . 3
c We NC 1c
AddC ⋃1 ∼ SI S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c1 1 1 NC c We NC NC Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
254 | | imor 401 |
. . . 4
c We NC NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c c We NC NC Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
255 | 254 | abbii 2465 |
. . 3
c We NC NC Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c
c We NC NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
256 | 1, 253, 255 | 3eqtr4i 2383 |
. 2
c We NC 1c
AddC ⋃1 ∼ SI S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c1 1 1 NC
c We NC NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
257 | | abexv 4324 |
. . 3
c We NC |
258 | | 2ndex 5112 |
. . . . . 6
|
259 | | 1stex 4739 |
. . . . . . . 8
|
260 | 259 | cnvex 5102 |
. . . . . . 7
|
261 | | snex 4111 |
. . . . . . 7
1c |
262 | 260, 261 | imaex 4747 |
. . . . . 6
1c |
263 | 258, 262 | resex 5117 |
. . . . 5
1c
|
264 | | addcfnex 5824 |
. . . . . 6
AddC |
265 | 264 | cnvex 5102 |
. . . . 5
AddC |
266 | 263, 265 | coex 4750 |
. . . 4
1c AddC |
267 | | ssetex 4744 |
. . . . . . . . . . . . 13
S |
268 | 267 | ins3ex 5798 |
. . . . . . . . . . . . . . . . . 18
Ins3 S |
269 | 267 | complex 4104 |
. . . . . . . . . . . . . . . . . . . . . . 23
∼ S |
270 | 269 | cnvex 5102 |
. . . . . . . . . . . . . . . . . . . . . 22
∼ S |
271 | 267 | cnvex 5102 |
. . . . . . . . . . . . . . . . . . . . . . 23
S
|
272 | 45 | imageex 5801 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Image
NC NC 2c ↑c
|
273 | 267, 272 | coex 4750 |
. . . . . . . . . . . . . . . . . . . . . . . 24
S
Image
NC NC 2c ↑c
|
274 | 273 | fixex 5789 |
. . . . . . . . . . . . . . . . . . . . . . 23
S Image
NC NC 2c ↑c
|
275 | 271, 274 | resex 5117 |
. . . . . . . . . . . . . . . . . . . . . 22
S S Image
NC NC 2c ↑c
|
276 | 270, 275 | txpex 5785 |
. . . . . . . . . . . . . . . . . . . . 21
∼ S S S Image
NC NC 2c ↑c
|
277 | 276 | rnex 5107 |
. . . . . . . . . . . . . . . . . . . 20
∼ S S S Image
NC NC 2c ↑c
|
278 | 277 | complex 4104 |
. . . . . . . . . . . . . . . . . . 19
∼ ∼ S S S Image
NC NC 2c ↑c
|
279 | 278 | ins2ex 5797 |
. . . . . . . . . . . . . . . . . 18
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
|
280 | 268, 279 | symdifex 4108 |
. . . . . . . . . . . . . . . . 17
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
|
281 | 280, 125 | imaex 4747 |
. . . . . . . . . . . . . . . 16
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c |
282 | 281 | complex 4104 |
. . . . . . . . . . . . . . 15
∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c |
283 | 282 | cnvex 5102 |
. . . . . . . . . . . . . 14
∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c |
284 | 283 | siex 4753 |
. . . . . . . . . . . . 13
SI ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c |
285 | 267, 284 | coex 4750 |
. . . . . . . . . . . 12
S
SI ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c |
286 | 285 | cnvex 5102 |
. . . . . . . . . . 11
S
SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c |
287 | | ncsex 6111 |
. . . . . . . . . . 11
NC |
288 | 286, 287 | resex 5117 |
. . . . . . . . . 10
S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC |
289 | 288 | cnvex 5102 |
. . . . . . . . 9
S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC |
290 | 289 | siex 4753 |
. . . . . . . 8
SI S
SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC |
291 | | tcfnex 6243 |
. . . . . . . . . . . . 13
TcFn |
292 | 291 | cnvex 5102 |
. . . . . . . . . . . 12
TcFn |
293 | 292 | siex 4753 |
. . . . . . . . . . 11
SI TcFn |
294 | 293 | siex 4753 |
. . . . . . . . . 10
SI SI TcFn |
295 | 258 | cnvex 5102 |
. . . . . . . . . . . . . . . . . . 19
|
296 | 295, 261 | imaex 4747 |
. . . . . . . . . . . . . . . . . 18
1c |
297 | 259, 296 | resex 5117 |
. . . . . . . . . . . . . . . . 17
1c
|
298 | 297 | cnvex 5102 |
. . . . . . . . . . . . . . . 16
1c |
299 | 264, 298 | coex 4750 |
. . . . . . . . . . . . . . 15
AddC 1c |
300 | | snex 4111 |
. . . . . . . . . . . . . . . . . . 19
2c |
301 | 295, 300 | imaex 4747 |
. . . . . . . . . . . . . . . . . 18
2c |
302 | 259, 301 | resex 5117 |
. . . . . . . . . . . . . . . . 17
2c
|
303 | 302 | cnvex 5102 |
. . . . . . . . . . . . . . . 16
2c |
304 | 264, 303 | coex 4750 |
. . . . . . . . . . . . . . 15
AddC 2c |
305 | 299, 304 | unex 4106 |
. . . . . . . . . . . . . 14
AddC
1c AddC 2c |
306 | 305 | cnvex 5102 |
. . . . . . . . . . . . 13
AddC 1c
AddC
2c |
307 | 292, 306 | coex 4750 |
. . . . . . . . . . . 12
TcFn AddC 1c AddC
2c |
308 | | nncex 4396 |
. . . . . . . . . . . 12
Nn |
309 | 307, 308 | resex 5117 |
. . . . . . . . . . 11
TcFn AddC 1c
AddC
2c Nn |
310 | 309, 289 | coex 4750 |
. . . . . . . . . 10
TcFn
AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC |
311 | 294, 310 | txpex 5785 |
. . . . . . . . 9
SI
SI TcFn TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC |
312 | 125 | pw1ex 4303 |
. . . . . . . . 9
1
1c
|
313 | 311, 312 | imaex 4747 |
. . . . . . . 8
SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c |
314 | 290, 313 | difex 4107 |
. . . . . . 7
SI
S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c |
315 | 287 | pw1ex 4303 |
. . . . . . . . 9
1 NC |
316 | 315 | pw1ex 4303 |
. . . . . . . 8
1 1 NC |
317 | 316 | pw1ex 4303 |
. . . . . . 7
1 1 1 NC |
318 | 314, 317 | imaex 4747 |
. . . . . 6
SI S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c1 1 1 NC |
319 | 318 | complex 4104 |
. . . . 5
∼ SI S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c1 1 1 NC |
320 | 319 | uni1ex 4293 |
. . . 4
⋃1 ∼ SI S
SI ∼
Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c1 1 1 NC |
321 | 266, 320 | imaex 4747 |
. . 3
1c AddC ⋃1 ∼ SI S
SI ∼ Ins3 S Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c1 1 1 NC |
322 | 257, 321 | unex 4106 |
. 2
c We NC 1c
AddC ⋃1 ∼ SI S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC SI SI TcFn
TcFn AddC 1c
AddC
2c Nn S SI ∼ Ins3 S
Ins2 ∼ ∼
S S S Image NC NC 2c ↑c
1c NC 1 1c1 1 1 NC |
323 | 256, 322 | eqeltrri 2424 |
1
c We NC NC Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |