NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  nchoicelem11 Unicode version
Theorem nchoicelem11 6300
Description: Lemma for nchoice 6309. Set up stratification for nchoicelem12 6301. (Contributed by SF, 18-Mar-2015.)
Assertion
Ref Expression
nchoicelem11 NC Nc Spac Tc Nc Spac Nn
Distinct variable group:   ,
Proof of Theorem nchoicelem11
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2863 . . . . 5
21elcompl 3226 . . . 4 ∼ NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI SI TcFn 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin 1 1 1 NC NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI SI TcFn 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin 1 1 1 NC
3 elimapw13 4947 . . . . . . 7 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI SI TcFn 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin 1 1 1 NC NC NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI SI TcFn 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin
4 tccl 6161 . . . . . . . . . . . . . 14 NC Tc NC
5 spacval 6283 . . . . . . . . . . . . . 14 Tc NC Spac Tc Clos1 Tc NC NC 2c ↑c
64, 5syl 15 . . . . . . . . . . . . 13 NC Spac Tc Clos1 Tc NC NC 2c ↑c
76nceqd 6111 . . . . . . . . . . . 12 NC Nc Spac Tc Nc Clos1 Tc NC NC 2c ↑c
87eqeq2d 2364 . . . . . . . . . . 11 NC Nc Spac Tc Nc Clos1 Tc NC NC 2c ↑c
9 finnc 6244 . . . . . . . . . . . 12 Spac Fin Nc Spac Nn
10 spacval 6283 . . . . . . . . . . . . 13 NC Spac Clos1 NC NC 2c ↑c
1110eleq1d 2419 . . . . . . . . . . . 12 NC Spac Fin Clos1 NC NC 2c ↑c Fin
129, 11syl5bbr 250 . . . . . . . . . . 11 NC Nc Spac Nn Clos1 NC NC 2c ↑c Fin
138, 12imbi12d 311 . . . . . . . . . 10 NC Nc Spac Tc Nc Spac Nn Nc Clos1 Tc NC NC 2c ↑c Clos1 NC NC 2c ↑c Fin
1413notbid 285 . . . . . . . . 9 NC Nc Spac Tc Nc Spac Nn Nc Clos1 Tc NC NC 2c ↑c Clos1 NC NC 2c ↑c Fin
15 eldif 3222 . . . . . . . . . 10 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI SI TcFn 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI SI TcFn 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin
16 opelco 4885 . . . . . . . . . . . . . 14 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI SI TcFn SI SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
17 snex 4112 . . . . . . . . . . . . . . . . . . 19
1817brsnsi1 5776 . . . . . . . . . . . . . . . . . 18 SI SI TcFn SI TcFn
1918anbi1i 676 . . . . . . . . . . . . . . . . 17 SI SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
20 19.41v 1901 . . . . . . . . . . . . . . . . . 18 SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
2120bicomi 193 . . . . . . . . . . . . . . . . 17 SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
2219, 21bitri 240 . . . . . . . . . . . . . . . 16 SI SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
2322exbii 1582 . . . . . . . . . . . . . . 15 SI SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
24 excom 1741 . . . . . . . . . . . . . . . 16 SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
25 anass 630 . . . . . . . . . . . . . . . . . . . 20 SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
2625exbii 1582 . . . . . . . . . . . . . . . . . . 19 SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
27 snex 4112 . . . . . . . . . . . . . . . . . . . 20
28 breq1 4643 . . . . . . . . . . . . . . . . . . . . 21 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
2928anbi2d 684 . . . . . . . . . . . . . . . . . . . 20 SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
3027, 29ceqsexv 2895 . . . . . . . . . . . . . . . . . . 19 SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
3126, 30bitri 240 . . . . . . . . . . . . . . . . . 18 SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
3231exbii 1582 . . . . . . . . . . . . . . . . 17 SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
33 snex 4112 . . . . . . . . . . . . . . . . . . . . . 22
3433brsnsi1 5776 . . . . . . . . . . . . . . . . . . . . 21 SI TcFn TcFn
3534anbi1i 676 . . . . . . . . . . . . . . . . . . . 20 SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
36 19.41v 1901 . . . . . . . . . . . . . . . . . . . 20 TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
3735, 36bitr4i 243 . . . . . . . . . . . . . . . . . . 19 SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
3837exbii 1582 . . . . . . . . . . . . . . . . . 18 SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
39 excom 1741 . . . . . . . . . . . . . . . . . . 19 TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
40 anass 630 . . . . . . . . . . . . . . . . . . . . . 22 TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
4140exbii 1582 . . . . . . . . . . . . . . . . . . . . 21 TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
42 snex 4112 . . . . . . . . . . . . . . . . . . . . . 22
43 sneq 3745 . . . . . . . . . . . . . . . . . . . . . . . 24
4443breq1d 4650 . . . . . . . . . . . . . . . . . . . . . . 23 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
4544anbi2d 684 . . . . . . . . . . . . . . . . . . . . . 22 TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
4642, 45ceqsexv 2895 . . . . . . . . . . . . . . . . . . . . 21 TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
4741, 46bitri 240 . . . . . . . . . . . . . . . . . . . 20 TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
4847exbii 1582 . . . . . . . . . . . . . . . . . . 19 TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
4939, 48bitri 240 . . . . . . . . . . . . . . . . . 18 TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
5038, 49bitri 240 . . . . . . . . . . . . . . . . 17 SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
5132, 50bitri 240 . . . . . . . . . . . . . . . 16 SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
5224, 51bitri 240 . . . . . . . . . . . . . . 15 SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
5323, 52bitri 240 . . . . . . . . . . . . . 14 SI SI TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
5416, 53bitri 240 . . . . . . . . . . . . 13 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI SI TcFn TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
55 vex 2863 . . . . . . . . . . . . . . . 16
5655brtcfn 6247 . . . . . . . . . . . . . . 15 TcFn Tc
57 df-br 4641 . . . . . . . . . . . . . . . . 17 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
58 opelcnv 4894 . . . . . . . . . . . . . . . . . 18 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
59 elin 3220 . . . . . . . . . . . . . . . . . . 19 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
60 snex 4112 . . . . . . . . . . . . . . . . . . . . 21
61 opelxp 4812 . . . . . . . . . . . . . . . . . . . . 21 NC NC
6260, 61mpbiran2 885 . . . . . . . . . . . . . . . . . . . 20 NC NC
63 ancom 437 . . . . . . . . . . . . . . . . . . . . . . . . . 26 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
6442brsnsi2 5777 . . . . . . . . . . . . . . . . . . . . . . . . . . 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
6564anbi1i 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
6663, 65bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . 25 S 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 S
67 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . 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
6866, 67bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . 24 S 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 S
6968exbii 1582 . . . . . . . . . . . . . . . . . . . . . . 23 S 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 S
70 excom 1741 . . . . . . . . . . . . . . . . . . . . . . 23 ∼ 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
7169, 70bitri 240 . . . . . . . . . . . . . . . . . . . . . 22 S 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 S
72 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
7372exbii 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
74 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . 26
75 breq2 4644 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 S S
7675anbi2d 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
7774, 76ceqsexv 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
7873, 77bitri 240 . . . . . . . . . . . . . . . . . . . . . . . 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
79 df-br 4641 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c
80 spacvallem1 6282 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 NC NC 2c ↑c
8180, 42nchoicelem10 6299 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Clos1 NC NC 2c ↑c
8279, 81bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . 25 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Clos1 NC NC 2c ↑c
83 brcnv 4893 . . . . . . . . . . . . . . . . . . . . . . . . . 26 S S
84 vex 2863 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8584, 1brssetsn 4760 . . . . . . . . . . . . . . . . . . . . . . . . . 26 S
8683, 85bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . 25 S
8782, 86anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . 24 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S Clos1 NC NC 2c ↑c
8878, 87bitri 240 . . . . . . . . . . . . . . . . . . . . . . 23 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S Clos1 NC NC 2c ↑c
8988exbii 1582 . . . . . . . . . . . . . . . . . . . . . 22 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S Clos1 NC NC 2c ↑c
9071, 89bitri 240 . . . . . . . . . . . . . . . . . . . . 21 S SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Clos1 NC NC 2c ↑c
91 opelco 4885 . . . . . . . . . . . . . . . . . . . . 21 SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S S SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c
92 df-clel 2349 . . . . . . . . . . . . . . . . . . . . 21 Clos1 NC NC 2c ↑c Clos1 NC NC 2c ↑c
9390, 91, 923bitr4i 268 . . . . . . . . . . . . . . . . . . . 20 SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S Clos1 NC NC 2c ↑c
9462, 93anbi12i 678 . . . . . . . . . . . . . . . . . . 19 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S NC Clos1 NC NC 2c ↑c
9559, 94bitri 240 . . . . . . . . . . . . . . . . . 18 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S NC Clos1 NC NC 2c ↑c
9658, 95bitri 240 . . . . . . . . . . . . . . . . 17 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S NC Clos1 NC NC 2c ↑c
9757, 96bitri 240 . . . . . . . . . . . . . . . 16 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S NC Clos1 NC NC 2c ↑c
9842, 80clos1ex 5877 . . . . . . . . . . . . . . . . 17 Clos1 NC NC 2c ↑c
9998eqnc2 6130 . . . . . . . . . . . . . . . 16 Nc Clos1 NC NC 2c ↑c NC Clos1 NC NC 2c ↑c
10097, 99bitr4i 243 . . . . . . . . . . . . . . 15 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S Nc Clos1 NC NC 2c ↑c
10156, 100anbi12i 678 . . . . . . . . . . . . . 14 TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S Tc Nc Clos1 NC NC 2c ↑c
102101exbii 1582 . . . . . . . . . . . . 13 TcFn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S Tc Nc Clos1 NC NC 2c ↑c
10354, 102bitri 240 . . . . . . . . . . . 12 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI SI TcFn Tc Nc Clos1 NC NC 2c ↑c
104 tcex 6158 . . . . . . . . . . . . 13 Tc
105 sneq 3745 . . . . . . . . . . . . . . . 16 Tc Tc
106 clos1eq1 5875 . . . . . . . . . . . . . . . 16 Tc Clos1 NC NC 2c ↑c Clos1 Tc NC NC 2c ↑c
107105, 106syl 15 . . . . . . . . . . . . . . 15 Tc Clos1 NC NC 2c ↑c Clos1 Tc NC NC 2c ↑c
108107nceqd 6111 . . . . . . . . . . . . . 14 Tc Nc Clos1 NC NC 2c ↑c Nc Clos1 Tc NC NC 2c ↑c
109108eqeq2d 2364 . . . . . . . . . . . . 13 Tc Nc Clos1 NC NC 2c ↑c Nc Clos1 Tc NC NC 2c ↑c
110104, 109ceqsexv 2895 . . . . . . . . . . . 12 Tc Nc Clos1 NC NC 2c ↑c Nc Clos1 Tc NC NC 2c ↑c
111103, 110bitri 240 . . . . . . . . . . 11 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI SI TcFn Nc Clos1 Tc NC NC 2c ↑c
112 df-br 4641 . . . . . . . . . . . . . . 15 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c
11380, 33nchoicelem10 6299 . . . . . . . . . . . . . . 15 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Clos1 NC NC 2c ↑c
114112, 113bitri 240 . . . . . . . . . . . . . 14 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Clos1 NC NC 2c ↑c
115114rexbii 2640 . . . . . . . . . . . . 13 Fin ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin Clos1 NC NC 2c ↑c
116 opelxp 4812 . . . . . . . . . . . . . . 15 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin
1171, 116mpbiran2 885 . . . . . . . . . . . . . 14 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin
118 snelpw1 4147 . . . . . . . . . . . . . . 15 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin
119 snelpw1 4147 . . . . . . . . . . . . . . . 16 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin
120 elima 4755 . . . . . . . . . . . . . . . 16 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin Fin ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c
121119, 120bitri 240 . . . . . . . . . . . . . . 15 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin Fin ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c
122118, 121bitri 240 . . . . . . . . . . . . . 14 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin Fin ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c
123117, 122bitri 240 . . . . . . . . . . . . 13 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin Fin ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c
124 risset 2662 . . . . . . . . . . . . 13 Clos1 NC NC 2c ↑c Fin Fin Clos1 NC NC 2c ↑c
125115, 123, 1243bitr4i 268 . . . . . . . . . . . 12 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin Clos1 NC NC 2c ↑c Fin
126125notbii 287 . . . . . . . . . . 11 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin Clos1 NC NC 2c ↑c Fin
127111, 126anbi12i 678 . . . . . . . . . 10 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI SI TcFn 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin Nc Clos1 Tc NC NC 2c ↑c Clos1 NC NC 2c ↑c Fin
128 annim 414 . . . . . . . . . 10 Nc Clos1 Tc NC NC 2c ↑c Clos1 NC NC 2c ↑c Fin Nc Clos1 Tc NC NC 2c ↑c Clos1 NC NC 2c ↑c Fin
12915, 127, 1283bitri 262 . . . . . . . . 9 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI SI TcFn 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin Nc Clos1 Tc NC NC 2c ↑c Clos1 NC NC 2c ↑c Fin
13014, 129syl6rbbr 255 . . . . . . . 8 NC NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI SI TcFn 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin Nc Spac Tc Nc Spac Nn
131130rexbiia 2648 . . . . . . 7 NC NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI SI TcFn 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin NC Nc Spac Tc Nc Spac Nn
1323, 131bitri 240 . . . . . 6 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI SI TcFn 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin 1 1 1 NC NC Nc Spac Tc Nc Spac Nn
133 rexnal 2626 . . . . . 6 NC Nc Spac Tc Nc Spac Nn NC Nc Spac Tc Nc Spac Nn
134132, 133bitr2i 241 . . . . 5 NC Nc Spac Tc Nc Spac Nn NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI SI TcFn 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin 1 1 1 NC
135134con1bii 321 . . . 4 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI SI TcFn 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin 1 1 1 NC NC Nc Spac Tc Nc Spac Nn
1362, 135bitri 240 . . 3 ∼ NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI SI TcFn 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin 1 1 1 NC NC Nc Spac Tc Nc Spac Nn
137136abbi2i 2465 . 2 ∼ NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI SI TcFn 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin 1 1 1 NC NC Nc Spac Tc Nc Spac Nn
138 ncsex 6112 . . . . . . . . 9 NC
139 vvex 4110 . . . . . . . . 9
140138, 139xpex 5116 . . . . . . . 8 NC
141 ssetex 4745 . . . . . . . . . . . . . 14 S
142141ins3ex 5799 . . . . . . . . . . . . 13 Ins3 S
143141complex 4105 . . . . . . . . . . . . . . . . . 18 ∼ S
144143cnvex 5103 . . . . . . . . . . . . . . . . 17 ∼ S
145141cnvex 5103 . . . . . . . . . . . . . . . . . 18 S
14680imageex 5802 . . . . . . . . . . . . . . . . . . . 20 Image NC NC 2c ↑c
147141, 146coex 4751 . . . . . . . . . . . . . . . . . . 19 S Image NC NC 2c ↑c
148147fixex 5790 . . . . . . . . . . . . . . . . . 18 S Image NC NC 2c ↑c
149145, 148resex 5118 . . . . . . . . . . . . . . . . 17 S S Image NC NC 2c ↑c
150144, 149txpex 5786 . . . . . . . . . . . . . . . 16 ∼ S S S Image NC NC 2c ↑c
151150rnex 5108 . . . . . . . . . . . . . . 15 ∼ S S S Image NC NC 2c ↑c
152151complex 4105 . . . . . . . . . . . . . 14 ∼ ∼ S S S Image NC NC 2c ↑c
153152ins2ex 5798 . . . . . . . . . . . . 13 Ins2 ∼ ∼ S S S Image NC NC 2c ↑c
154142, 153symdifex 4109 . . . . . . . . . . . 12 Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c
155 1cex 4143 . . . . . . . . . . . 12 1c
156154, 155imaex 4748 . . . . . . . . . . 11 Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c
157156complex 4105 . . . . . . . . . 10 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c
158157siex 4754 . . . . . . . . 9 SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c
159158, 145coex 4751 . . . . . . . 8 SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
160140, 159inex 4106 . . . . . . 7 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
161160cnvex 5103 . . . . . 6 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S
162 tcfnex 6245 . . . . . . . 8 TcFn
163162siex 4754 . . . . . . 7 SI TcFn
164163siex 4754 . . . . . 6 SI SI TcFn
165161, 164coex 4751 . . . . 5 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI SI TcFn
166 finex 4398 . . . . . . . . 9 Fin
167157, 166imaex 4748 . . . . . . . 8 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin
168167pw1ex 4304 . . . . . . 7 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin
169168pw1ex 4304 . . . . . 6 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin
170169, 139xpex 5116 . . . . 5 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin
171165, 170difex 4108 . . . 4 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI SI TcFn 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin
172138pw1ex 4304 . . . . . 6 1 NC
173172pw1ex 4304 . . . . 5 1 1 NC
174173pw1ex 4304 . . . 4 1 1 1 NC
175171, 174imaex 4748 . . 3 NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI SI TcFn 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin 1 1 1 NC
176175complex 4105 . 2 ∼ NC SI ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c S SI SI TcFn 1 1 ∼ Ins3 S Ins2 ∼ ∼ S S S Image NC NC 2c ↑c 1c Fin 1 1 1 NC
177137, 176eqeltrri 2424 1 NC Nc Spac Tc Nc Spac Nn
Colors of variables: wff setvar class
Syntax hints:   wn 3   wi 4   wa 358   w3a 934  wex 1541   wceq 1642   wcel 1710  cab 2339  wral 2615  wrex 2616  cvv 2860   ∼ ccompl 3206   cdif 3207   cin 3209   csymdif 3210  csn 3738  1cc1c 4135  1 cpw1 4136   Nn cnnc 4374   Fin cfin 4377  cop 4562  copab 4623   class class class wbr 4640   S csset 4720   SI csi 4721   ccom 4722  cima 4723   cxp 4771  ccnv 4772   crn 4774   cres 4775  cfv 4782  (class class class)co 5526   ctxp 5736  cfix 5740   Ins2 cins2 5750   Ins3 cins3 5752  Imagecimage 5754   Clos1 cclos1 5873   NC cncs 6089   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-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-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-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:  nchoicelem12  6301
  Copyright terms: Public domain W3C validator