NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  nchoicelem16 Unicode version
Theorem nchoicelem16 6305
Description: Lemma for nchoice 6309. Set up stratification for nchoicelem17 6306. (Contributed by SF, 19-Mar-2015.)
Assertion
Ref Expression
nchoicelem16 <_c We NC NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
Distinct variable group:   ,
Proof of Theorem nchoicelem16
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 unab 3522 . . 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 4757 . . . . . 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 2863 . . . . . . . . . . 11
43eluni1 4174 . . . . . . . . . 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 4112 . . . . . . . . . . 11
65elcompl 3226 . . . . . . . . . 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 4947 . . . . . . . . . . . 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 6283 . . . . . . . . . . . . . . . . . 18 NC Spac Clos1 NC NC 2c ↑c
98nceqd 6111 . . . . . . . . . . . . . . . . 17 NC Nc Spac Nc Clos1 NC NC 2c ↑c
109eqeq1d 2361 . . . . . . . . . . . . . . . 16 NC Nc Spac Nc Clos1 NC NC 2c ↑c
11 tccl 6161 . . . . . . . . . . . . . . . . . . . 20 NC Tc NC
12 spacval 6283 . . . . . . . . . . . . . . . . . . . 20 Tc NC Spac Tc Clos1 Tc NC NC 2c ↑c
1311, 12syl 15 . . . . . . . . . . . . . . . . . . 19 NC Spac Tc Clos1 Tc NC NC 2c ↑c
1413eleq1d 2419 . . . . . . . . . . . . . . . . . 18 NC Spac Tc Fin Clos1 Tc NC NC 2c ↑c Fin
1513nceqd 6111 . . . . . . . . . . . . . . . . . . . 20 NC Nc Spac Tc Nc Clos1 Tc NC NC 2c ↑c
1615eqeq1d 2361 . . . . . . . . . . . . . . . . . . 19 NC Nc Spac Tc Tc 1c Nc Clos1 Tc NC NC 2c ↑c Tc 1c
1715eqeq1d 2361 . . . . . . . . . . . . . . . . . . 19 NC Nc Spac Tc Tc 2c Nc Clos1 Tc NC NC 2c ↑c Tc 2c
1816, 17orbi12d 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
1914, 18anbi12d 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
2019notbid 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
2110, 20anbi12d 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 3222 . . . . . . . . . . . . . . . 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 4112 . . . . . . . . . . . . . . . . . . . 20
2423, 3opsnelsi 5775 . . . . . . . . . . . . . . . . . . 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 4894 . . . . . . . . . . . . . . . . . . 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 4951 . . . . . . . . . . . . . . . . . . . 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 4894 . . . . . . . . . . . . . . . . . . . . . 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 4885 . . . . . . . . . . . . . . . . . . . . . . 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 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3029brsnsi1 5776 . . . . . . . . . . . . . . . . . . . . . . . . . . 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
3130anbi1i 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
3331, 32bitr4i 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
3433exbii 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
3634, 35bitri 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
3837exbii 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 4112 . . . . . . . . . . . . . . . . . . . . . . . . . 26
40 breq1 4643 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 S S
4140anbi2d 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
4239, 41ceqsexv 2895 . . . . . . . . . . . . . . . . . . . . . . . . 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 4893 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4641 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6282 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 NC NC 2c ↑c
4645, 29nchoicelem10 6299 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Clos1 NC NC 2c ↑c
4743, 44, 463bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Clos1 NC NC 2c ↑c
48 vex 2863 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4948, 3brssetsn 4760 . . . . . . . . . . . . . . . . . . . . . . . . . 26 S
5047, 49anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . 25 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S Clos1 NC NC 2c ↑c
5138, 42, 503bitri 262 . . . . . . . . . . . . . . . . . . . . . . . 24 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S Clos1 NC NC 2c ↑c
5251exbii 1582 . . . . . . . . . . . . . . . . . . . . . . 23 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S Clos1 NC NC 2c ↑c
5328, 36, 523bitri 262 . . . . . . . . . . . . . . . . . . . . . 22 S SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Clos1 NC NC 2c ↑c
5429, 45clos1ex 5877 . . . . . . . . . . . . . . . . . . . . . . 23 Clos1 NC NC 2c ↑c
55 eleq1 2413 . . . . . . . . . . . . . . . . . . . . . . 23 Clos1 NC NC 2c ↑c Clos1 NC NC 2c ↑c
5654, 55ceqsexv 2895 . . . . . . . . . . . . . . . . . . . . . 22 Clos1 NC NC 2c ↑c Clos1 NC NC 2c ↑c
5727, 53, 563bitri 262 . . . . . . . . . . . . . . . . . . . . 21 S SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Clos1 NC NC 2c ↑c
5857anbi1i 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
6026, 58, 593bitri 262 . . . . . . . . . . . . . . . . . . 19 S SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c NC NC Clos1 NC NC 2c ↑c
6124, 25, 603bitri 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
6354eqnc2 6130 . . . . . . . . . . . . . . . . . . 19 Nc Clos1 NC NC 2c ↑c NC Clos1 NC NC 2c ↑c
6462, 63bitri 240 . . . . . . . . . . . . . . . . . 18 Nc Clos1 NC NC 2c ↑c NC Clos1 NC NC 2c ↑c
6561, 64bitr4i 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 4949 . . . . . . . . . . . . . . . . . . 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 5783 . . . . . . . . . . . . . . . . . . . . 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 4112 . . . . . . . . . . . . . . . . . . . . . . . 24
6968, 23opsnelsi 5775 . . . . . . . . . . . . . . . . . . . . . . 23 SI SI TcFn SI TcFn
70 vex 2863 . . . . . . . . . . . . . . . . . . . . . . . . 25
7170, 29opsnelsi 5775 . . . . . . . . . . . . . . . . . . . . . . . 24 SI TcFn TcFn
72 df-br 4641 . . . . . . . . . . . . . . . . . . . . . . . 24 TcFn TcFn
73 brcnv 4893 . . . . . . . . . . . . . . . . . . . . . . . 24 TcFn TcFn
7471, 72, 733bitr2i 264 . . . . . . . . . . . . . . . . . . . . . . 23 SI TcFn TcFn
75 vex 2863 . . . . . . . . . . . . . . . . . . . . . . . 24
7675brtcfn 6247 . . . . . . . . . . . . . . . . . . . . . . 23 TcFn Tc
7769, 74, 763bitri 262 . . . . . . . . . . . . . . . . . . . . . 22 SI SI TcFn Tc
78 opelco 4885 . . . . . . . . . . . . . . . . . . . . . . 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 4893 . . . . . . . . . . . . . . . . . . . . . . . . . 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 4950 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
8368brsnsi1 5776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
8483anbi1i 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
8684, 85bitr4i 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
8786exbii 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
9089exbii 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 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
92 breq1 4643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 S S
9392anbi2d 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
9491, 93ceqsexv 2895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
9745, 68nchoicelem10 6299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Clos1 NC NC 2c ↑c
9895, 96, 973bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Clos1 NC NC 2c ↑c
99 vex 2863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
10099, 48brssetsn 4760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 S
10198, 100anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S Clos1 NC NC 2c ↑c
10290, 94, 1013bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S Clos1 NC NC 2c ↑c
103102exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S Clos1 NC NC 2c ↑c
10487, 88, 1033bitri 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
106104, 105bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S Clos1 NC NC 2c ↑c
10781, 82, 1063bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 S SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Clos1 NC NC 2c ↑c
108107anbi1i 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
11080, 108, 1093bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 S SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c NC NC Clos1 NC NC 2c ↑c
11168, 45clos1ex 5877 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Clos1 NC NC 2c ↑c
112111eqnc2 6130 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Nc Clos1 NC NC 2c ↑c NC Clos1 NC NC 2c ↑c
113110, 112bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . 26 S SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c NC Nc Clos1 NC NC 2c ↑c
11479, 113bitri 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 4950 . . . . . . . . . . . . . . . . . . . . . . . . . 26 TcFn AddC 1c AddC 2c Nn TcFn AddC 1c AddC 2c Nn
116 brco 4884 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 TcFn AddC 1c AddC 2c AddC 1c AddC 2c TcFn
117 brcnv 4893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 AddC 1c AddC 2c AddC 1c AddC 2c
118 brun 4693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 AddC 1c AddC 2c AddC 1c AddC 2c
119 brco 4884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 AddC 1c 1c AddC
120 brcnv 4893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 1c 1c
121 brres 4950 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 1c 1c
122 eliniseg 5021 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 1c 1c
123122anbi2i 675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 1c 1c
124121, 123bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 1c 1c
125 1cex 4143 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 1c
12699, 125op1st2nd 5791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 1c 1c
127120, 124, 1263bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 1c 1c
128127anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 1c AddC 1c AddC
129128exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 1c AddC 1c AddC
13099, 125opex 4589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 1c
131 breq1 4643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 1c AddC 1c AddC
132130, 131ceqsexv 2895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 1c AddC 1c AddC
133119, 129, 1323bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 AddC 1c 1c AddC
13499, 125braddcfn 5827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 1c AddC 1c
135 eqcom 2355 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 1c 1c
136133, 134, 1353bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 AddC 1c 1c
137 brco 4884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 AddC 2c 2c AddC
138 brcnv 4893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 2c 2c
139 brres 4950 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 2c 2c
140 eliniseg 5021 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 2c 2c
141140anbi2i 675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 2c 2c
142139, 141bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 2c 2c
143 2nc 6169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 2c NC
144143elexi 2869 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 2c
14599, 144op1st2nd 5791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 2c 2c
146138, 142, 1453bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 2c 2c
147146anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 2c AddC 2c AddC
148147exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 2c AddC 2c AddC
14999, 144opex 4589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 2c
150 breq1 4643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 2c AddC 2c AddC
151149, 150ceqsexv 2895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 2c AddC 2c AddC
152137, 148, 1513bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 AddC 2c 2c AddC
15399, 144braddcfn 5827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 2c AddC 2c
154 eqcom 2355 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 2c 2c
155152, 153, 1543bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 AddC 2c 2c
156136, 155orbi12i 507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 AddC 1c AddC 2c 1c 2c
157117, 118, 1563bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 AddC 1c AddC 2c 1c 2c
158 brcnv 4893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 TcFn TcFn
1593brtcfn 6247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 TcFn Tc
160158, 159bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 TcFn Tc
161157, 160anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 AddC 1c AddC 2c TcFn 1c 2c Tc
162 ancom 437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 1c 2c Tc Tc 1c 2c
163161, 162bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 AddC 1c AddC 2c TcFn Tc 1c 2c
164163exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 AddC 1c AddC 2c TcFn Tc 1c 2c
165 tcex 6158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Tc
166 addceq1 4384 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Tc 1c Tc 1c
167166eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Tc 1c Tc 1c
168 addceq1 4384 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Tc 2c Tc 2c
169168eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Tc 2c Tc 2c
170167, 169orbi12d 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Tc 1c 2c Tc 1c Tc 2c
171165, 170ceqsexv 2895 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Tc 1c 2c Tc 1c Tc 2c
172116, 164, 1713bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 TcFn AddC 1c AddC 2c Tc 1c Tc 2c
173172anbi1i 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
175115, 173, 1743bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . 25 TcFn AddC 1c AddC 2c Nn Nn Tc 1c Tc 2c
176114, 175anbi12i 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
177176exbii 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 6118 . . . . . . . . . . . . . . . . . . . . . . . 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 6244 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Clos1 NC NC 2c ↑c Fin Nc Clos1 NC NC 2c ↑c Nn
181179, 180syl6bbr 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
184182, 183orbi12d 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
185181, 184anbi12d 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
186178, 185ceqsexv 2895 . . . . . . . . . . . . . . . . . . . . . . 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
18778, 177, 1863bitri 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
18877, 187anbi12i 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
18967, 188bitri 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
190189exbii 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 6158 . . . . . . . . . . . . . . . . . . . 20 Tc
192 sneq 3745 . . . . . . . . . . . . . . . . . . . . . . 23 Tc Tc
193 clos1eq1 5875 . . . . . . . . . . . . . . . . . . . . . . 23 Tc Clos1 NC NC 2c ↑c Clos1 Tc NC NC 2c ↑c
194192, 193syl 15 . . . . . . . . . . . . . . . . . . . . . 22 Tc Clos1 NC NC 2c ↑c Clos1 Tc NC NC 2c ↑c
195194eleq1d 2419 . . . . . . . . . . . . . . . . . . . . 21 Tc Clos1 NC NC 2c ↑c Fin Clos1 Tc NC NC 2c ↑c Fin
196194nceqd 6111 . . . . . . . . . . . . . . . . . . . . . . 23 Tc Nc Clos1 NC NC 2c ↑c Nc Clos1 Tc NC NC 2c ↑c
197196eqeq1d 2361 . . . . . . . . . . . . . . . . . . . . . 22 Tc Nc Clos1 NC NC 2c ↑c Tc 1c Nc Clos1 Tc NC NC 2c ↑c Tc 1c
198196eqeq1d 2361 . . . . . . . . . . . . . . . . . . . . . 22 Tc Nc Clos1 NC NC 2c ↑c Tc 2c Nc Clos1 Tc NC NC 2c ↑c Tc 2c
199197, 198orbi12d 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
200195, 199anbi12d 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
201191, 200ceqsexv 2895 . . . . . . . . . . . . . . . . . . 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
20266, 190, 2013bitri 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
203202notbii 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
20465, 203anbi12i 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
20522, 204bitri 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
20621, 205syl6rbbr 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 6159 . . . . . . . . . . . . . . . . . . . 20 Nc Spac Tc Nc Spac Tc
208207addceq1d 4390 . . . . . . . . . . . . . . . . . . 19 Nc Spac Tc Nc Spac 1c Tc 1c
209208eqeq2d 2364 . . . . . . . . . . . . . . . . . 18 Nc Spac Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc 1c
210207addceq1d 4390 . . . . . . . . . . . . . . . . . . 19 Nc Spac Tc Nc Spac 2c Tc 2c
211210eqeq2d 2364 . . . . . . . . . . . . . . . . . 18 Nc Spac Nc Spac Tc Tc Nc Spac 2c Nc Spac Tc Tc 2c
212209, 211orbi12d 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
213212anbi2d 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
214213notbid 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
215214pm5.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
216206, 215syl6bbr 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
217216rexbiia 2648 . . . . . . . . . . . 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 2661 . . . . . . . . . . . 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
2197, 217, 2183bitrri 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
220219con1bii 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
2214, 6, 2203bitri 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 4885 . . . . . . . . . . 11 1c AddC AddC 1c
223 brcnv 4893 . . . . . . . . . . . . . 14 AddC AddC
224 brres 4950 . . . . . . . . . . . . . . 15 1c 1c
225 eliniseg 5021 . . . . . . . . . . . . . . . . 17 1c 1c
226225anbi2i 675 . . . . . . . . . . . . . . . 16 1c 1c
227 ancom 437 . . . . . . . . . . . . . . . 16 1c 1c
228226, 227bitri 240 . . . . . . . . . . . . . . 15 1c 1c
229125, 99op1st2nd 5791 . . . . . . . . . . . . . . 15 1c 1c
230224, 228, 2293bitri 262 . . . . . . . . . . . . . 14 1c 1c
231223, 230anbi12i 678 . . . . . . . . . . . . 13 AddC 1c AddC 1c
232 ancom 437 . . . . . . . . . . . . 13 AddC 1c 1c AddC
233231, 232bitri 240 . . . . . . . . . . . 12 AddC 1c 1c AddC
234233exbii 1582 . . . . . . . . . . 11 AddC 1c 1c AddC
235125, 99opex 4589 . . . . . . . . . . . 12 1c
236 breq1 4643 . . . . . . . . . . . 12 1c AddC 1c AddC
237235, 236ceqsexv 2895 . . . . . . . . . . 11 1c AddC 1c AddC
238222, 234, 2373bitri 262 . . . . . . . . . 10 1c AddC 1c AddC
239125, 99braddcfn 5827 . . . . . . . . . 10 1c AddC 1c
240 eqcom 2355 . . . . . . . . . 10 1c 1c
241238, 239, 2403bitri 262 . . . . . . . . 9 1c AddC 1c
242221, 241anbi12i 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
244242, 243bitri 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
245244exbii 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
246125, 99addcex 4395 . . . . . . 7 1c
247 eqeq2 2362 . . . . . . . . 9 1c Nc Spac Nc Spac 1c
248247imbi1d 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
249248ralbidv 2635 . . . . . . 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
250246, 249ceqsexv 2895 . . . . . 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
2512, 245, 2503bitri 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
252251abbi2i 2465 . . . 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
253252uneq2i 3416 . . 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
255254abbii 2466 . . 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
2561, 253, 2553eqtr4i 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 4325 . . 3 <_c We NC
258 2ndex 5113 . . . . . 6
259 1stex 4740 . . . . . . . 8
260259cnvex 5103 . . . . . . 7
261 snex 4112 . . . . . . 7 1c
262260, 261imaex 4748 . . . . . 6 1c
263258, 262resex 5118 . . . . 5 1c
264 addcfnex 5825 . . . . . 6 AddC
265264cnvex 5103 . . . . 5 AddC
266263, 265coex 4751 . . . 4 1c AddC
267 ssetex 4745 . . . . . . . . . . . . 13 S
268267ins3ex 5799 . . . . . . . . . . . . . . . . . 18 Ins3 S
269267complex 4105 . . . . . . . . . . . . . . . . . . . . . . 23 ∼ S
270269cnvex 5103 . . . . . . . . . . . . . . . . . . . . . 22 ∼ S
271267cnvex 5103 . . . . . . . . . . . . . . . . . . . . . . 23 S
27245imageex 5802 . . . . . . . . . . . . . . . . . . . . . . . . 25 Image NC NC 2c ↑c
273267, 272coex 4751 . . . . . . . . . . . . . . . . . . . . . . . 24 S Image NC NC 2c ↑c
274273fixex 5790 . . . . . . . . . . . . . . . . . . . . . . 23 S Image NC NC 2c ↑c
275271, 274resex 5118 . . . . . . . . . . . . . . . . . . . . . 22 S S Image NC NC 2c ↑c
276270, 275txpex 5786 . . . . . . . . . . . . . . . . . . . . 21 ∼ S S S Image NC NC 2c ↑c
277276rnex 5108 . . . . . . . . . . . . . . . . . . . 20 ∼ S S S Image NC NC 2c ↑c
278277complex 4105 . . . . . . . . . . . . . . . . . . 19 ∼ ∼ S S S Image NC NC 2c ↑c
279278ins2ex 5798 . . . . . . . . . . . . . . . . . 18 Ins2 ∼ ∼ S S S Image NC NC 2c ↑c
280268, 279symdifex 4109 . . . . . . . . . . . . . . . . 17 Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c
281280, 125imaex 4748 . . . . . . . . . . . . . . . 16 Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c
282281complex 4105 . . . . . . . . . . . . . . 15 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c
283282cnvex 5103 . . . . . . . . . . . . . 14 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c
284283siex 4754 . . . . . . . . . . . . 13 SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c
285267, 284coex 4751 . . . . . . . . . . . 12 S SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c
286285cnvex 5103 . . . . . . . . . . 11 S SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c
287 ncsex 6112 . . . . . . . . . . 11 NC
288286, 287resex 5118 . . . . . . . . . 10 S SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c NC
289288cnvex 5103 . . . . . . . . 9 S SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c NC
290289siex 4754 . . . . . . . 8 SI S SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c NC
291 tcfnex 6245 . . . . . . . . . . . . 13 TcFn
292291cnvex 5103 . . . . . . . . . . . 12 TcFn
293292siex 4754 . . . . . . . . . . 11 SI TcFn
294293siex 4754 . . . . . . . . . 10 SI SI TcFn
295258cnvex 5103 . . . . . . . . . . . . . . . . . . 19
296295, 261imaex 4748 . . . . . . . . . . . . . . . . . 18 1c
297259, 296resex 5118 . . . . . . . . . . . . . . . . 17 1c
298297cnvex 5103 . . . . . . . . . . . . . . . 16 1c
299264, 298coex 4751 . . . . . . . . . . . . . . 15 AddC 1c
300 snex 4112 . . . . . . . . . . . . . . . . . . 19 2c
301295, 300imaex 4748 . . . . . . . . . . . . . . . . . 18 2c
302259, 301resex 5118 . . . . . . . . . . . . . . . . 17 2c
303302cnvex 5103 . . . . . . . . . . . . . . . 16 2c
304264, 303coex 4751 . . . . . . . . . . . . . . 15 AddC 2c
305299, 304unex 4107 . . . . . . . . . . . . . 14 AddC 1c AddC 2c
306305cnvex 5103 . . . . . . . . . . . . 13 AddC 1c AddC 2c
307292, 306coex 4751 . . . . . . . . . . . 12 TcFn AddC 1c AddC 2c
308 nncex 4397 . . . . . . . . . . . 12 Nn
309307, 308resex 5118 . . . . . . . . . . 11 TcFn AddC 1c AddC 2c Nn
310309, 289coex 4751 . . . . . . . . . 10 TcFn AddC 1c AddC 2c Nn S SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c NC
311294, 310txpex 5786 . . . . . . . . 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
312125pw1ex 4304 . . . . . . . . 9 1 1c
313311, 312imaex 4748 . . . . . . . 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
314290, 313difex 4108 . . . . . . 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
315287pw1ex 4304 . . . . . . . . 9 1 NC
316315pw1ex 4304 . . . . . . . 8 1 1 NC
317316pw1ex 4304 . . . . . . 7 1 1 1 NC
318314, 317imaex 4748 . . . . . 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
319318complex 4105 . . . . 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
320319uni1ex 4294 . . . 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
321266, 320imaex 4748 . . 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
322257, 321unex 4107 . 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
323256, 322eqeltrri 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
Colors of variables: wff setvar class
Syntax hints:   wn 3   wi 4   wo 357   wa 358   w3a 934  wex 1541   wceq 1642   wcel 1710  cab 2339  wral 2615  wrex 2616  cvv 2860   ∼ ccompl 3206   cdif 3207   cun 3208   csymdif 3210  csn 3738  ⋃1cuni1 4134  1cc1c 4135  1 cpw1 4136   Nn cnnc 4374   cplc 4376   Fin cfin 4377  cop 4562  copab 4623   class class class wbr 4640  c1st 4718   S csset 4720   SI csi 4721   ccom 4722  cima 4723  ccnv 4772   crn 4774   cres 4775  cfv 4782  c2nd 4784  (class class class)co 5526   ctxp 5736  cfix 5740   AddC caddcfn 5746   Ins2 cins2 5750   Ins3 cins3 5752  Imagecimage 5754   Clos1 cclos1 5873   We cwe 5896   NC cncs 6089   <_c clec 6090   Nc cnc 6092   Tc ctc 6094  2cc2c 6095   ↑c cce 6097  TcFnctcfn 6098   Spac cspac 6274
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-reu 2622  df-rmo 2623  df-rab 2624  df-v 2862  df-sbc 3048  df-csb 3138  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-pss 3262  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-iun 3972  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-idk 4196  df-iota 4340  df-0c 4378  df-addc 4379  df-nnc 4380  df-fin 4381  df-lefin 4441  df-ltfin 4442  df-ncfin 4443  df-tfin 4444  df-evenfin 4445  df-oddfin 4446  df-sfin 4447  df-spfin 4448  df-phi 4566  df-op 4567  df-proj1 4568  df-proj2 4569  df-opab 4624  df-br 4641  df-1st 4724  df-swap 4725  df-sset 4726  df-co 4727  df-ima 4728  df-si 4729  df-id 4768  df-xp 4785  df-cnv 4786  df-rn 4787  df-dm 4788  df-res 4789  df-fun 4790  df-fn 4791  df-f 4792  df-f1 4793  df-fo 4794  df-f1o 4795  df-fv 4796  df-2nd 4798  df-ov 5527  df-oprab 5529  df-mpt 5653  df-mpt2 5655  df-txp 5737  df-fix 5741  df-cup 5743  df-disj 5745  df-addcfn 5747  df-ins2 5751  df-ins3 5753  df-image 5755  df-ins4 5757  df-si3 5759  df-funs 5761  df-fns 5763  df-pw1fn 5767  df-fullfun 5769  df-clos1 5874  df-trans 5900  df-sym 5909  df-er 5910  df-ec 5948  df-qs 5952  df-map 6002  df-en 6030  df-ncs 6099  df-nc 6102  df-tc 6104  df-2c 6105  df-ce 6107  df-tcfn 6108  df-spac 6275
This theorem is referenced by:  nchoicelem17  6306
  Copyright terms: Public domain W3C validator