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

Theorem nmembers1lem1 6268
Description: Lemma for nmembers1 6271. Set up stratification. (Contributed by SF, 25-Mar-2015.)
Assertion
Ref Expression
nmembers1lem1 {x {m Nn (1cc m mc x)} Tc Tc x} V
Distinct variable group:   x,m

Proof of Theorem nmembers1lem1
Dummy variables p q y t are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2862 . . . . 5 x V
21eluni1 4173 . . . 4 (x 11ran ((( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) ∩ Ins3 S ) “ 1c) ↔ {x} 1ran ((( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) ∩ Ins3 S ) “ 1c))
3 snex 4111 . . . . 5 {x} V
43eluni1 4173 . . . 4 ({x} 1ran ((( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) ∩ Ins3 S ) “ 1c) ↔ {{x}} ran ((( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) ∩ Ins3 S ) “ 1c))
5 elrn2 4897 . . . . . 6 ({{x}} ran ((( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) ∩ Ins3 S ) “ 1c) ↔ qq, {{x}} ((( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) ∩ Ins3 S ) “ 1c))
6 elima1c 4947 . . . . . . . 8 (q, {{x}} ((( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) ∩ Ins3 S ) “ 1c) ↔ p{p}, q, {{x}} (( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) ∩ Ins3 S ))
7 elin 3219 . . . . . . . . . . . 12 ({p}, q, {{x}} ( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) ↔ ({p}, q, {{x}} Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) {p}, q, {{x}} (V × ( SI TcFn TcFn))))
8 vex 2862 . . . . . . . . . . . . . . 15 q V
98otelins2 5791 . . . . . . . . . . . . . 14 ({p}, q, {{x}} Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ↔ {p}, {{x}} SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c))
10 vex 2862 . . . . . . . . . . . . . . 15 p V
1110, 3opsnelsi 5774 . . . . . . . . . . . . . 14 ({p}, {{x}} SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ↔ p, {x} ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c))
12 opelres 4950 . . . . . . . . . . . . . . . . 17 (y, x (( ≤c ( ≤c “ {1c})) Nn ) ↔ (y, x ( ≤c ( ≤c “ {1c})) y Nn ))
13 ancom 437 . . . . . . . . . . . . . . . . 17 ((y, x ( ≤c ( ≤c “ {1c})) y Nn ) ↔ (y Nn y, x ( ≤c ( ≤c “ {1c}))))
14 df-br 4640 . . . . . . . . . . . . . . . . . . 19 (y( ≤c ( ≤c “ {1c}))xy, x ( ≤c ( ≤c “ {1c})))
15 brres 4949 . . . . . . . . . . . . . . . . . . . 20 (y( ≤c ( ≤c “ {1c}))x ↔ (yc x y ( ≤c “ {1c})))
16 ancom 437 . . . . . . . . . . . . . . . . . . . 20 ((yc x y ( ≤c “ {1c})) ↔ (y ( ≤c “ {1c}) yc x))
17 elimasn 5019 . . . . . . . . . . . . . . . . . . . . . 22 (y ( ≤c “ {1c}) ↔ 1c, y c )
18 df-br 4640 . . . . . . . . . . . . . . . . . . . . . 22 (1cc y1c, y c )
1917, 18bitr4i 243 . . . . . . . . . . . . . . . . . . . . 21 (y ( ≤c “ {1c}) ↔ 1cc y)
2019anbi1i 676 . . . . . . . . . . . . . . . . . . . 20 ((y ( ≤c “ {1c}) yc x) ↔ (1cc y yc x))
2115, 16, 203bitri 262 . . . . . . . . . . . . . . . . . . 19 (y( ≤c ( ≤c “ {1c}))x ↔ (1cc y yc x))
2214, 21bitr3i 242 . . . . . . . . . . . . . . . . . 18 (y, x ( ≤c ( ≤c “ {1c})) ↔ (1cc y yc x))
2322anbi2i 675 . . . . . . . . . . . . . . . . 17 ((y Nn y, x ( ≤c ( ≤c “ {1c}))) ↔ (y Nn (1cc y yc x)))
2412, 13, 233bitri 262 . . . . . . . . . . . . . . . 16 (y, x (( ≤c ( ≤c “ {1c})) Nn ) ↔ (y Nn (1cc y yc x)))
25 vex 2862 . . . . . . . . . . . . . . . . 17 y V
2625, 1opsnelsi 5774 . . . . . . . . . . . . . . . 16 ({y}, {x} SI (( ≤c ( ≤c “ {1c})) Nn ) ↔ y, x (( ≤c ( ≤c “ {1c})) Nn ))
27 breq2 4643 . . . . . . . . . . . . . . . . . 18 (m = y → (1cc m ↔ 1cc y))
28 breq1 4642 . . . . . . . . . . . . . . . . . 18 (m = y → (mc xyc x))
2927, 28anbi12d 691 . . . . . . . . . . . . . . . . 17 (m = y → ((1cc m mc x) ↔ (1cc y yc x)))
3029elrab 2994 . . . . . . . . . . . . . . . 16 (y {m Nn (1cc m mc x)} ↔ (y Nn (1cc y yc x)))
3124, 26, 303bitr4i 268 . . . . . . . . . . . . . . 15 ({y}, {x} SI (( ≤c ( ≤c “ {1c})) Nn ) ↔ y {m Nn (1cc m mc x)})
323, 31releqel 5807 . . . . . . . . . . . . . 14 (p, {x} ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ↔ p = {m Nn (1cc m mc x)})
339, 11, 323bitri 262 . . . . . . . . . . . . 13 ({p}, q, {{x}} Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ↔ p = {m Nn (1cc m mc x)})
34 snex 4111 . . . . . . . . . . . . . . 15 {p} V
35 opelxp 4811 . . . . . . . . . . . . . . 15 ({p}, q, {{x}} (V × ( SI TcFn TcFn)) ↔ ({p} V q, {{x}} ( SI TcFn TcFn)))
3634, 35mpbiran 884 . . . . . . . . . . . . . 14 ({p}, q, {{x}} (V × ( SI TcFn TcFn)) ↔ q, {{x}} ( SI TcFn TcFn))
37 opelco 4884 . . . . . . . . . . . . . 14 (q, {{x}} ( SI TcFn TcFn) ↔ t(qTcFnt t SI TcFn{{x}}))
383brsnsi2 5776 . . . . . . . . . . . . . . . . . 18 (t SI TcFn{{x}} ↔ p(t = {p} pTcFn{x}))
3938anbi2i 675 . . . . . . . . . . . . . . . . 17 ((qTcFnt t SI TcFn{{x}}) ↔ (qTcFnt p(t = {p} pTcFn{x})))
40 19.42v 1905 . . . . . . . . . . . . . . . . 17 (p(qTcFnt (t = {p} pTcFn{x})) ↔ (qTcFnt p(t = {p} pTcFn{x})))
4139, 40bitr4i 243 . . . . . . . . . . . . . . . 16 ((qTcFnt t SI TcFn{{x}}) ↔ p(qTcFnt (t = {p} pTcFn{x})))
4241exbii 1582 . . . . . . . . . . . . . . 15 (t(qTcFnt t SI TcFn{{x}}) ↔ tp(qTcFnt (t = {p} pTcFn{x})))
43 excom 1741 . . . . . . . . . . . . . . 15 (tp(qTcFnt (t = {p} pTcFn{x})) ↔ pt(qTcFnt (t = {p} pTcFn{x})))
44 an12 772 . . . . . . . . . . . . . . . . . . 19 ((qTcFnt (t = {p} pTcFn{x})) ↔ (t = {p} (qTcFnt pTcFn{x})))
4544exbii 1582 . . . . . . . . . . . . . . . . . 18 (t(qTcFnt (t = {p} pTcFn{x})) ↔ t(t = {p} (qTcFnt pTcFn{x})))
46 breq2 4643 . . . . . . . . . . . . . . . . . . . 20 (t = {p} → (qTcFntqTcFn{p}))
4746anbi1d 685 . . . . . . . . . . . . . . . . . . 19 (t = {p} → ((qTcFnt pTcFn{x}) ↔ (qTcFn{p} pTcFn{x})))
4834, 47ceqsexv 2894 . . . . . . . . . . . . . . . . . 18 (t(t = {p} (qTcFnt pTcFn{x})) ↔ (qTcFn{p} pTcFn{x}))
4945, 48bitri 240 . . . . . . . . . . . . . . . . 17 (t(qTcFnt (t = {p} pTcFn{x})) ↔ (qTcFn{p} pTcFn{x}))
5049exbii 1582 . . . . . . . . . . . . . . . 16 (pt(qTcFnt (t = {p} pTcFn{x})) ↔ p(qTcFn{p} pTcFn{x}))
51 brcnv 4892 . . . . . . . . . . . . . . . . . . . 20 (qTcFn{p} ↔ {p}TcFnq)
5210brtcfn 6246 . . . . . . . . . . . . . . . . . . . 20 ({p}TcFnqq = Tc p)
5351, 52bitri 240 . . . . . . . . . . . . . . . . . . 19 (qTcFn{p} ↔ q = Tc p)
54 brcnv 4892 . . . . . . . . . . . . . . . . . . . 20 (pTcFn{x} ↔ {x}TcFnp)
551brtcfn 6246 . . . . . . . . . . . . . . . . . . . 20 ({x}TcFnpp = Tc x)
5654, 55bitri 240 . . . . . . . . . . . . . . . . . . 19 (pTcFn{x} ↔ p = Tc x)
5753, 56anbi12i 678 . . . . . . . . . . . . . . . . . 18 ((qTcFn{p} pTcFn{x}) ↔ (q = Tc p p = Tc x))
58 ancom 437 . . . . . . . . . . . . . . . . . 18 ((q = Tc p p = Tc x) ↔ (p = Tc x q = Tc p))
5957, 58bitri 240 . . . . . . . . . . . . . . . . 17 ((qTcFn{p} pTcFn{x}) ↔ (p = Tc x q = Tc p))
6059exbii 1582 . . . . . . . . . . . . . . . 16 (p(qTcFn{p} pTcFn{x}) ↔ p(p = Tc x q = Tc p))
61 tcex 6157 . . . . . . . . . . . . . . . . 17 Tc x V
62 tceq 6158 . . . . . . . . . . . . . . . . . 18 (p = Tc xTc p = Tc Tc x)
6362eqeq2d 2364 . . . . . . . . . . . . . . . . 17 (p = Tc x → (q = Tc pq = Tc Tc x))
6461, 63ceqsexv 2894 . . . . . . . . . . . . . . . 16 (p(p = Tc x q = Tc p) ↔ q = Tc Tc x)
6550, 60, 643bitri 262 . . . . . . . . . . . . . . 15 (pt(qTcFnt (t = {p} pTcFn{x})) ↔ q = Tc Tc x)
6642, 43, 653bitri 262 . . . . . . . . . . . . . 14 (t(qTcFnt t SI TcFn{{x}}) ↔ q = Tc Tc x)
6736, 37, 663bitri 262 . . . . . . . . . . . . 13 ({p}, q, {{x}} (V × ( SI TcFn TcFn)) ↔ q = Tc Tc x)
6833, 67anbi12i 678 . . . . . . . . . . . 12 (({p}, q, {{x}} Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) {p}, q, {{x}} (V × ( SI TcFn TcFn))) ↔ (p = {m Nn (1cc m mc x)} q = Tc Tc x))
697, 68bitri 240 . . . . . . . . . . 11 ({p}, q, {{x}} ( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) ↔ (p = {m Nn (1cc m mc x)} q = Tc Tc x))
70 snex 4111 . . . . . . . . . . . . 13 {{x}} V
7170otelins3 5792 . . . . . . . . . . . 12 ({p}, q, {{x}} Ins3 S {p}, q S )
7210, 8opelssetsn 4760 . . . . . . . . . . . 12 ({p}, q S p q)
7371, 72bitri 240 . . . . . . . . . . 11 ({p}, q, {{x}} Ins3 S p q)
7469, 73anbi12i 678 . . . . . . . . . 10 (({p}, q, {{x}} ( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) {p}, q, {{x}} Ins3 S ) ↔ ((p = {m Nn (1cc m mc x)} q = Tc Tc x) p q))
75 elin 3219 . . . . . . . . . 10 ({p}, q, {{x}} (( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) ∩ Ins3 S ) ↔ ({p}, q, {{x}} ( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) {p}, q, {{x}} Ins3 S ))
76 df-3an 936 . . . . . . . . . 10 ((p = {m Nn (1cc m mc x)} q = Tc Tc x p q) ↔ ((p = {m Nn (1cc m mc x)} q = Tc Tc x) p q))
7774, 75, 763bitr4i 268 . . . . . . . . 9 ({p}, q, {{x}} (( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) ∩ Ins3 S ) ↔ (p = {m Nn (1cc m mc x)} q = Tc Tc x p q))
7877exbii 1582 . . . . . . . 8 (p{p}, q, {{x}} (( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) ∩ Ins3 S ) ↔ p(p = {m Nn (1cc m mc x)} q = Tc Tc x p q))
796, 78bitri 240 . . . . . . 7 (q, {{x}} ((( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) ∩ Ins3 S ) “ 1c) ↔ p(p = {m Nn (1cc m mc x)} q = Tc Tc x p q))
8079exbii 1582 . . . . . 6 (qq, {{x}} ((( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) ∩ Ins3 S ) “ 1c) ↔ qp(p = {m Nn (1cc m mc x)} q = Tc Tc x p q))
815, 80bitri 240 . . . . 5 ({{x}} ran ((( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) ∩ Ins3 S ) “ 1c) ↔ qp(p = {m Nn (1cc m mc x)} q = Tc Tc x p q))
82 excom 1741 . . . . 5 (qp(p = {m Nn (1cc m mc x)} q = Tc Tc x p q) ↔ pq(p = {m Nn (1cc m mc x)} q = Tc Tc x p q))
83 imasn 5018 . . . . . . . . . . 11 ( ≤c “ {1c}) = {m 1cc m}
84 iniseg 5022 . . . . . . . . . . 11 (c “ {x}) = {m mc x}
8583, 84ineq12i 3455 . . . . . . . . . 10 (( ≤c “ {1c}) ∩ (c “ {x})) = ({m 1cc m} ∩ {m mc x})
86 inab 3522 . . . . . . . . . 10 ({m 1cc m} ∩ {m mc x}) = {m (1cc m mc x)}
8785, 86eqtri 2373 . . . . . . . . 9 (( ≤c “ {1c}) ∩ (c “ {x})) = {m (1cc m mc x)}
8887ineq1i 3453 . . . . . . . 8 ((( ≤c “ {1c}) ∩ (c “ {x})) ∩ Nn ) = ({m (1cc m mc x)} ∩ Nn )
89 dfrab2 3530 . . . . . . . 8 {m Nn (1cc m mc x)} = ({m (1cc m mc x)} ∩ Nn )
9088, 89eqtr4i 2376 . . . . . . 7 ((( ≤c “ {1c}) ∩ (c “ {x})) ∩ Nn ) = {m Nn (1cc m mc x)}
91 lecex 6115 . . . . . . . . . 10 c V
92 snex 4111 . . . . . . . . . 10 {1c} V
9391, 92imaex 4747 . . . . . . . . 9 ( ≤c “ {1c}) V
9491cnvex 5102 . . . . . . . . . 10 c V
9594, 3imaex 4747 . . . . . . . . 9 (c “ {x}) V
9693, 95inex 4105 . . . . . . . 8 (( ≤c “ {1c}) ∩ (c “ {x})) V
97 nncex 4396 . . . . . . . 8 Nn V
9896, 97inex 4105 . . . . . . 7 ((( ≤c “ {1c}) ∩ (c “ {x})) ∩ Nn ) V
9990, 98eqeltrri 2424 . . . . . 6 {m Nn (1cc m mc x)} V
100 tcex 6157 . . . . . 6 Tc Tc x V
101 eleq1 2413 . . . . . 6 (p = {m Nn (1cc m mc x)} → (p q ↔ {m Nn (1cc m mc x)} q))
102 eleq2 2414 . . . . . 6 (q = Tc Tc x → ({m Nn (1cc m mc x)} q ↔ {m Nn (1cc m mc x)} Tc Tc x))
10399, 100, 101, 102ceqsex2v 2896 . . . . 5 (pq(p = {m Nn (1cc m mc x)} q = Tc Tc x p q) ↔ {m Nn (1cc m mc x)} Tc Tc x)
10481, 82, 1033bitri 262 . . . 4 ({{x}} ran ((( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) ∩ Ins3 S ) “ 1c) ↔ {m Nn (1cc m mc x)} Tc Tc x)
1052, 4, 1043bitri 262 . . 3 (x 11ran ((( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) ∩ Ins3 S ) “ 1c) ↔ {m Nn (1cc m mc x)} Tc Tc x)
106105abbi2i 2464 . 2 11ran ((( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) ∩ Ins3 S ) “ 1c) = {x {m Nn (1cc m mc x)} Tc Tc x}
107 ssetex 4744 . . . . . . . . . . . . . 14 S V
108107ins3ex 5798 . . . . . . . . . . . . 13 Ins3 S V
10991, 93resex 5117 . . . . . . . . . . . . . . . 16 ( ≤c ( ≤c “ {1c})) V
110109, 97resex 5117 . . . . . . . . . . . . . . 15 (( ≤c ( ≤c “ {1c})) Nn ) V
111110siex 4753 . . . . . . . . . . . . . 14 SI (( ≤c ( ≤c “ {1c})) Nn ) V
112111ins2ex 5797 . . . . . . . . . . . . 13 Ins2 SI (( ≤c ( ≤c “ {1c})) Nn ) V
113108, 112symdifex 4108 . . . . . . . . . . . 12 ( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) V
114 1cex 4142 . . . . . . . . . . . 12 1c V
115113, 114imaex 4747 . . . . . . . . . . 11 (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) V
116115complex 4104 . . . . . . . . . 10 ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) V
117116siex 4753 . . . . . . . . 9 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) V
118117ins2ex 5797 . . . . . . . 8 Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) V
119 vvex 4109 . . . . . . . . 9 V V
120 tcfnex 6244 . . . . . . . . . . . 12 TcFn V
121120cnvex 5102 . . . . . . . . . . 11 TcFn V
122121siex 4753 . . . . . . . . . 10 SI TcFn V
123122, 121coex 4750 . . . . . . . . 9 ( SI TcFn TcFn) V
124119, 123xpex 5115 . . . . . . . 8 (V × ( SI TcFn TcFn)) V
125118, 124inex 4105 . . . . . . 7 ( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) V
126125, 108inex 4105 . . . . . 6 (( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) ∩ Ins3 S ) V
127126, 114imaex 4747 . . . . 5 ((( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) ∩ Ins3 S ) “ 1c) V
128127rnex 5107 . . . 4 ran ((( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) ∩ Ins3 S ) “ 1c) V
129128uni1ex 4293 . . 3 1ran ((( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) ∩ Ins3 S ) “ 1c) V
130129uni1ex 4293 . 2 11ran ((( Ins2 SI ∼ (( Ins3 S Ins2 SI (( ≤c ( ≤c “ {1c})) Nn )) “ 1c) ∩ (V × ( SI TcFn TcFn))) ∩ Ins3 S ) “ 1c) V
131106, 130eqeltrri 2424 1 {x {m Nn (1cc m mc x)} Tc Tc x} V
Colors of variables: wff setvar class
Syntax hints:   wa 358   w3a 934  wex 1541   = wceq 1642   wcel 1710  {cab 2339  {crab 2618  Vcvv 2859  ccompl 3205  cin 3208  csymdif 3209  {csn 3737  1cuni1 4133  1cc1c 4134   Nn cnnc 4373  cop 4561   class class class wbr 4639   S csset 4719   SI csi 4720   ccom 4721  cima 4722   × cxp 4770  ccnv 4771  ran crn 4773   cres 4774   Ins2 cins2 5749   Ins3 cins3 5751  c clec 6089   Tc ctc 6093  TcFnctcfn 6097
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 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-lec 6099  df-nc 6101  df-tc 6103  df-tcfn 6107
This theorem is referenced by:  nmembers1  6271
  Copyright terms: Public domain W3C validator