NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  nchoicelem16 Unicode version
Theorem nchoicelem16 6304
Description: Lemma for nchoice 6308. Set up stratification for nchoicelem17 6305. (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 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
43eluni1 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
65elcompl 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 6282 . . . . . . . . . . . . . . . . . 18 NC Spac Clos1 NC NC 2c ↑c
98nceqd 6110 . . . . . . . . . . . . . . . . 17 NC Nc Spac Nc Clos1 NC NC 2c ↑c
109eqeq1d 2361 . . . . . . . . . . . . . . . 16 NC Nc Spac Nc Clos1 NC NC 2c ↑c
11 tccl 6160 . . . . . . . . . . . . . . . . . . . 20 NC Tc NC
12 spacval 6282 . . . . . . . . . . . . . . . . . . . 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 6110 . . . . . . . . . . . . . . . . . . . 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 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
2423, 3opsnelsi 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
3029brsnsi1 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
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 4111 . . . . . . . . . . . . . . . . . . . . . . . . . 26
40 breq1 4642 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 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 6281 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 NC NC 2c ↑c
4645, 29nchoicelem10 6298 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4948, 3brssetsn 4759 . . . . . . . . . . . . . . . . . . . . . . . . . 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 5876 . . . . . . . . . . . . . . . . . . . . . . 23 Clos1 NC NC 2c ↑c
55 eleq1 2413 . . . . . . . . . . . . . . . . . . . . . . 23 Clos1 NC NC 2c ↑c Clos1 NC NC 2c ↑c
5654, 55ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . 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 6129 . . . . . . . . . . . . . . . . . . 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 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
6968, 23opsnelsi 5774 . . . . . . . . . . . . . . . . . . . . . . 23 SI SI TcFn SI TcFn
70 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . 25
7170, 29opsnelsi 5774 . . . . . . . . . . . . . . . . . . . . . . . 24 SI TcFn TcFn
72 df-br 4640 . . . . . . . . . . . . . . . . . . . . . . . 24 TcFn TcFn
73 brcnv 4892 . . . . . . . . . . . . . . . . . . . . . . . 24 TcFn TcFn
7471, 72, 733bitr2i 264 . . . . . . . . . . . . . . . . . . . . . . 23 SI TcFn TcFn
75 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . 24
7675brtcfn 6246 . . . . . . . . . . . . . . . . . . . . . . 23 TcFn Tc
7769, 74, 763bitri 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
8368brsnsi1 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
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 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
92 breq1 4642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 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
9745, 68nchoicelem10 6298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
10099, 48brssetsn 4759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Clos1 NC NC 2c ↑c
112111eqnc2 6129 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 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
123122anbi2i 675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 1c 1c
124121, 123bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 1c 1c
125 1cex 4142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 1c
12699, 125op1st2nd 5790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 1c
131 breq1 4642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 1c AddC 1c AddC
132130, 131ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 1c AddC 1c AddC
133119, 129, 1323bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 AddC 1c 1c AddC
13499, 125braddcfn 5826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 1c AddC 1c
135 eqcom 2355 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 1c 1c
136133, 134, 1353bitri 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
141140anbi2i 675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 2c 2c
142139, 141bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 2c 2c
143 2nc 6168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 2c NC
144143elexi 2868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 2c
14599, 144op1st2nd 5790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 2c
150 breq1 4642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 2c AddC 2c AddC
151149, 150ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 2c AddC 2c AddC
152137, 148, 1513bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 AddC 2c 2c AddC
15399, 144braddcfn 5826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 TcFn TcFn
1593brtcfn 6246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Tc
166 addceq1 4383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Tc 1c Tc 1c
167166eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Tc 1c Tc 1c
168 addceq1 4383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 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 6243 . . . . . . . . . . . . . . . . . . . . . . . . . 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 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
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 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
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 6110 . . . . . . . . . . . . . . . . . . . . . . 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