New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  tcfnex GIF version

Theorem tcfnex 6244
 Description: The stratified T raising function is a set. (Contributed by SF, 18-Mar-2015.)
Assertion
Ref Expression
tcfnex TcFn V

Proof of Theorem tcfnex
Dummy variables q p x z y t u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-tcfn 6107 . . 3 TcFn = (x 1c Tc x)
2 oteltxp 5782 . . . . . . 7 (z, {y}, x ( S ⊗ ∼ ran ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I )) ↔ (z, {y} S z, x ∼ ran ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I )))
3 df-br 4640 . . . . . . . . 9 (z S {y} ↔ z, {y} S )
4 brcnv 4892 . . . . . . . . . 10 (z S {y} ↔ {y} S z)
5 vex 2862 . . . . . . . . . . 11 y V
6 vex 2862 . . . . . . . . . . 11 z V
75, 6brssetsn 4759 . . . . . . . . . 10 ({y} S zy z)
84, 7bitri 240 . . . . . . . . 9 (z S {y} ↔ y z)
93, 8bitr3i 242 . . . . . . . 8 (z, {y} S y z)
10 vex 2862 . . . . . . . . . . 11 x V
116, 10opex 4588 . . . . . . . . . 10 z, x V
1211elcompl 3225 . . . . . . . . 9 (z, x ∼ ran ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I ) ↔ ¬ z, x ran ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I ))
13 elrn2 4897 . . . . . . . . . . 11 (z, x ran ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I ) ↔ pp, z, x ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I ))
14 elsymdif 3223 . . . . . . . . . . . . 13 (p, z, x ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I ) ↔ ¬ (p, z, x Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ↔ p, z, x Ins3 I ))
156otelins2 5791 . . . . . . . . . . . . . . 15 (p, z, x Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ↔ p, x (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)))
16 elin 3219 . . . . . . . . . . . . . . 15 (p, x (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ↔ (p, x ( NC × V) p, x ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)))
17 opelxp 4811 . . . . . . . . . . . . . . . . . 18 (p, x ( NC × V) ↔ (p NC x V))
1810, 17mpbiran2 885 . . . . . . . . . . . . . . . . 17 (p, x ( NC × V) ↔ p NC )
1918anbi1i 676 . . . . . . . . . . . . . . . 16 ((p, x ( NC × V) p, x ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ↔ (p NC p, x ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)))
20 ncseqnc 6128 . . . . . . . . . . . . . . . . . . 19 (p NC → (p = Nc 1q1q p))
2120rexbidv 2635 . . . . . . . . . . . . . . . . . 18 (p NC → (q xp = Nc 1qq x1q p))
22 oteltxp 5782 . . . . . . . . . . . . . . . . . . . . 21 ({{q}}, p, x (( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) ↔ ({{q}}, p ( S SI Pw1Fn ) {{q}}, x (( SI S S ) “ 1c)))
23 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {q} V
2423brsnsi1 5775 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({{q}} SI Pw1Fn ut(u = {t} {q} Pw1Fn t))
2524anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (({{q}} SI Pw1Fn u u S p) ↔ (t(u = {t} {q} Pw1Fn t) u S p))
26 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (t((u = {t} {q} Pw1Fn t) u S p) ↔ (t(u = {t} {q} Pw1Fn t) u S p))
2725, 26bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . 25 (({{q}} SI Pw1Fn u u S p) ↔ t((u = {t} {q} Pw1Fn t) u S p))
2827exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . 24 (u({{q}} SI Pw1Fn u u S p) ↔ ut((u = {t} {q} Pw1Fn t) u S p))
29 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . 24 (ut((u = {t} {q} Pw1Fn t) u S p) ↔ tu((u = {t} {q} Pw1Fn t) u S p))
30 anass 630 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((u = {t} {q} Pw1Fn t) u S p) ↔ (u = {t} ({q} Pw1Fn t u S p)))
3130exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (u((u = {t} {q} Pw1Fn t) u S p) ↔ u(u = {t} ({q} Pw1Fn t u S p)))
32 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {t} V
33 breq1 4642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (u = {t} → (u S p ↔ {t} S p))
3433anbi2d 684 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (u = {t} → (({q} Pw1Fn t u S p) ↔ ({q} Pw1Fn t {t} S p)))
3532, 34ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (u(u = {t} ({q} Pw1Fn t u S p)) ↔ ({q} Pw1Fn t {t} S p))
36 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 q V
3736brpw1fn 5854 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({q} Pw1Fn tt = 1q)
38 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 t V
39 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 p V
4038, 39brssetsn 4759 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({t} S pt p)
4137, 40anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (({q} Pw1Fn t {t} S p) ↔ (t = 1q t p))
4231, 35, 413bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . 25 (u((u = {t} {q} Pw1Fn t) u S p) ↔ (t = 1q t p))
4342exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . 24 (tu((u = {t} {q} Pw1Fn t) u S p) ↔ t(t = 1q t p))
4428, 29, 433bitri 262 . . . . . . . . . . . . . . . . . . . . . . 23 (u({{q}} SI Pw1Fn u u S p) ↔ t(t = 1q t p))
45 opelco 4884 . . . . . . . . . . . . . . . . . . . . . . 23 ({{q}}, p ( S SI Pw1Fn ) ↔ u({{q}} SI Pw1Fn u u S p))
46 df-clel 2349 . . . . . . . . . . . . . . . . . . . . . . 23 (1q pt(t = 1q t p))
4744, 45, 463bitr4i 268 . . . . . . . . . . . . . . . . . . . . . 22 ({{q}}, p ( S SI Pw1Fn ) ↔ 1q p)
48 oteltxp 5782 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({t}, {{q}}, x ( SI S S ) ↔ ({t}, {{q}} SI S {t}, x S ))
49 df-br 4640 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({t} SI S {{q}} ↔ {t}, {{q}} SI S )
5038, 23brsnsi 5773 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ({t} SI S {{q}} ↔ t S {q})
51 brcnv 4892 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (t S {q} ↔ {q} S t)
5236, 38brssetsn 4759 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ({q} S tq t)
5350, 51, 523bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({t} SI S {{q}} ↔ q t)
5449, 53bitr3i 242 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({t}, {{q}} SI S q t)
5538, 10opelssetsn 4760 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({t}, x S t x)
5654, 55anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . 25 (({t}, {{q}} SI S {t}, x S ) ↔ (q t t x))
5748, 56bitri 240 . . . . . . . . . . . . . . . . . . . . . . . 24 ({t}, {{q}}, x ( SI S S ) ↔ (q t t x))
5857exbii 1582 . . . . . . . . . . . . . . . . . . . . . . 23 (t{t}, {{q}}, x ( SI S S ) ↔ t(q t t x))
59 elima1c 4947 . . . . . . . . . . . . . . . . . . . . . . 23 ({{q}}, x (( SI S S ) “ 1c) ↔ t{t}, {{q}}, x ( SI S S ))
60 eluni 3894 . . . . . . . . . . . . . . . . . . . . . . 23 (q xt(q t t x))
6158, 59, 603bitr4i 268 . . . . . . . . . . . . . . . . . . . . . 22 ({{q}}, x (( SI S S ) “ 1c) ↔ q x)
6247, 61anbi12i 678 . . . . . . . . . . . . . . . . . . . . 21 (({{q}}, p ( S SI Pw1Fn ) {{q}}, x (( SI S S ) “ 1c)) ↔ (1q p q x))
63 ancom 437 . . . . . . . . . . . . . . . . . . . . 21 ((1q p q x) ↔ (q x 1q p))
6422, 62, 633bitri 262 . . . . . . . . . . . . . . . . . . . 20 ({{q}}, p, x (( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) ↔ (q x 1q p))
6564exbii 1582 . . . . . . . . . . . . . . . . . . 19 (q{{q}}, p, x (( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) ↔ q(q x 1q p))
66 elimapw11c 4948 . . . . . . . . . . . . . . . . . . 19 (p, x ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c) ↔ q{{q}}, p, x (( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)))
67 df-rex 2620 . . . . . . . . . . . . . . . . . . 19 (q x1q pq(q x 1q p))
6865, 66, 673bitr4i 268 . . . . . . . . . . . . . . . . . 18 (p, x ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c) ↔ q x1q p)
6921, 68syl6rbbr 255 . . . . . . . . . . . . . . . . 17 (p NC → (p, x ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c) ↔ q xp = Nc 1q))
7069pm5.32i 618 . . . . . . . . . . . . . . . 16 ((p NC p, x ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ↔ (p NC q xp = Nc 1q))
7119, 70bitri 240 . . . . . . . . . . . . . . 15 ((p, x ( NC × V) p, x ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ↔ (p NC q xp = Nc 1q))
7215, 16, 713bitri 262 . . . . . . . . . . . . . 14 (p, z, x Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ↔ (p NC q xp = Nc 1q))
7310otelins3 5792 . . . . . . . . . . . . . . 15 (p, z, x Ins3 I ↔ p, z I )
74 df-br 4640 . . . . . . . . . . . . . . . 16 (p I zp, z I )
756ideq 4870 . . . . . . . . . . . . . . . 16 (p I zp = z)
7674, 75bitr3i 242 . . . . . . . . . . . . . . 15 (p, z I ↔ p = z)
7773, 76bitri 240 . . . . . . . . . . . . . 14 (p, z, x Ins3 I ↔ p = z)
7872, 77bibi12i 306 . . . . . . . . . . . . 13 ((p, z, x Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ↔ p, z, x Ins3 I ) ↔ ((p NC q xp = Nc 1q) ↔ p = z))
7914, 78xchbinx 301 . . . . . . . . . . . 12 (p, z, x ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I ) ↔ ¬ ((p NC q xp = Nc 1q) ↔ p = z))
8079exbii 1582 . . . . . . . . . . 11 (pp, z, x ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I ) ↔ p ¬ ((p NC q xp = Nc 1q) ↔ p = z))
81 exnal 1574 . . . . . . . . . . 11 (p ¬ ((p NC q xp = Nc 1q) ↔ p = z) ↔ ¬ p((p NC q xp = Nc 1q) ↔ p = z))
8213, 80, 813bitrri 263 . . . . . . . . . 10 p((p NC q xp = Nc 1q) ↔ p = z) ↔ z, x ran ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I ))
8382con1bii 321 . . . . . . . . 9 z, x ran ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I ) ↔ p((p NC q xp = Nc 1q) ↔ p = z))
8412, 83bitri 240 . . . . . . . 8 (z, x ∼ ran ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I ) ↔ p((p NC q xp = Nc 1q) ↔ p = z))
859, 84anbi12i 678 . . . . . . 7 ((z, {y} S z, x ∼ ran ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I )) ↔ (y z p((p NC q xp = Nc 1q) ↔ p = z)))
862, 85bitri 240 . . . . . 6 (z, {y}, x ( S ⊗ ∼ ran ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I )) ↔ (y z p((p NC q xp = Nc 1q) ↔ p = z)))
8786exbii 1582 . . . . 5 (zz, {y}, x ( S ⊗ ∼ ran ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I )) ↔ z(y z p((p NC q xp = Nc 1q) ↔ p = z)))
88 elrn2 4897 . . . . 5 ({y}, x ran ( S ⊗ ∼ ran ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I )) ↔ zz, {y}, x ( S ⊗ ∼ ran ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I )))
89 df-tc 6103 . . . . . . . 8 Tc x = (℩p(p NC q xp = Nc 1q))
90 dfiota2 4340 . . . . . . . 8 (℩p(p NC q xp = Nc 1q)) = {z p((p NC q xp = Nc 1q) ↔ p = z)}
9189, 90eqtri 2373 . . . . . . 7 Tc x = {z p((p NC q xp = Nc 1q) ↔ p = z)}
9291eleq2i 2417 . . . . . 6 (y Tc xy {z p((p NC q xp = Nc 1q) ↔ p = z)})
93 eluniab 3903 . . . . . 6 (y {z p((p NC q xp = Nc 1q) ↔ p = z)} ↔ z(y z p((p NC q xp = Nc 1q) ↔ p = z)))
9492, 93bitri 240 . . . . 5 (y Tc xz(y z p((p NC q xp = Nc 1q) ↔ p = z)))
9587, 88, 943bitr4i 268 . . . 4 ({y}, x ran ( S ⊗ ∼ ran ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I )) ↔ y Tc x)
9695releqmpt 5808 . . 3 ((1c × V) ∩ ∼ (( Ins3 S Ins2 ran ( S ⊗ ∼ ran ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I ))) “ 1c)) = (x 1c Tc x)
971, 96eqtr4i 2376 . 2 TcFn = ((1c × V) ∩ ∼ (( Ins3 S Ins2 ran ( S ⊗ ∼ ran ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I ))) “ 1c))
98 1cex 4142 . . 3 1c V
99 ssetex 4744 . . . . . 6 S V
10099cnvex 5102 . . . . 5 S V
101 ncsex 6111 . . . . . . . . . . 11 NC V
102 vvex 4109 . . . . . . . . . . 11 V V
103101, 102xpex 5115 . . . . . . . . . 10 ( NC × V) V
104 pw1fnex 5852 . . . . . . . . . . . . . 14 Pw1Fn V
105104siex 4753 . . . . . . . . . . . . 13 SI Pw1Fn V
10699, 105coex 4750 . . . . . . . . . . . 12 ( S SI Pw1Fn ) V
107100siex 4753 . . . . . . . . . . . . . 14 SI S V
108107, 99txpex 5785 . . . . . . . . . . . . 13 ( SI S S ) V
109108, 98imaex 4747 . . . . . . . . . . . 12 (( SI S S ) “ 1c) V
110106, 109txpex 5785 . . . . . . . . . . 11 (( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) V
11198pw1ex 4303 . . . . . . . . . . 11 11c V
112110, 111imaex 4747 . . . . . . . . . 10 ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c) V
113103, 112inex 4105 . . . . . . . . 9 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) V
114113ins2ex 5797 . . . . . . . 8 Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) V
115 idex 5504 . . . . . . . . 9 I V
116115ins3ex 5798 . . . . . . . 8 Ins3 I V
117114, 116symdifex 4108 . . . . . . 7 ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I ) V
118117rnex 5107 . . . . . 6 ran ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I ) V
119118complex 4104 . . . . 5 ∼ ran ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I ) V
120100, 119txpex 5785 . . . 4 ( S ⊗ ∼ ran ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I )) V
121120rnex 5107 . . 3 ran ( S ⊗ ∼ ran ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I )) V
12298, 121mptexlem 5810 . 2 ((1c × V) ∩ ∼ (( Ins3 S Ins2 ran ( S ⊗ ∼ ran ( Ins2 (( NC × V) ∩ ((( S SI Pw1Fn ) ⊗ (( SI S S ) “ 1c)) “ 11c)) ⊕ Ins3 I ))) “ 1c)) V
12397, 122eqeltri 2423 1 TcFn V
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 176   ∧ wa 358  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710  {cab 2339  ∃wrex 2615  Vcvv 2859   ∼ ccompl 3205   ∩ cin 3208   ⊕ csymdif 3209  {csn 3737  ∪cuni 3891  1cc1c 4134  ℘1cpw1 4135  ℩cio 4337  ⟨cop 4561   class class class wbr 4639   S csset 4719   SI csi 4720   ∘ ccom 4721   “ cima 4722   I cid 4763   × cxp 4770  ◡ccnv 4771  ran crn 4773   ↦ cmpt 5651   ⊗ ctxp 5735   Ins2 cins2 5749   Ins3 cins3 5751   Pw1Fn cpw1fn 5765   NC cncs 6088   Nc cnc 6091   Tc ctc 6093  TcFnctcfn 6097 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087 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 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-pss 3261  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380  df-lefin 4440  df-ltfin 4441  df-ncfin 4442  df-tfin 4443  df-evenfin 4444  df-oddfin 4445  df-sfin 4446  df-spfin 4447  df-phi 4565  df-op 4566  df-proj1 4567  df-proj2 4568  df-opab 4623  df-br 4640  df-1st 4723  df-swap 4724  df-sset 4725  df-co 4726  df-ima 4727  df-si 4728  df-id 4767  df-xp 4784  df-cnv 4785  df-rn 4786  df-dm 4787  df-res 4788  df-fun 4789  df-fn 4790  df-f 4791  df-f1 4792  df-fo 4793  df-f1o 4794  df-fv 4795  df-2nd 4797  df-mpt 5652  df-txp 5736  df-ins2 5750  df-ins3 5752  df-image 5754  df-ins4 5756  df-si3 5758  df-funs 5760  df-fns 5762  df-pw1fn 5766  df-trans 5899  df-sym 5908  df-er 5909  df-ec 5947  df-qs 5951  df-en 6029  df-ncs 6098  df-nc 6101  df-tc 6103  df-tcfn 6107 This theorem is referenced by:  nmembers1lem1  6268  nchoicelem11  6299  nchoicelem16  6304
 Copyright terms: Public domain W3C validator