Theorem nchoicelem10 6299

Description: Lemma for nchoice 6309. Stratification helper lemma. (Contributed by SF, 18-Mar-2015.)

Hypotheses

Ref	Expression
nchoicelem10.1	|- S e. _V
nchoicelem10.2	|- X e. _V

Assertion

Ref	Expression
nchoicelem10	|- (<.c, X>. e. ∼ (( Ins3 S (+) Ins2 ∼ ran (`' ∼ S (x) (`' S |` Fix( S o. ImageS))))"1c) <-> c = Clos1 (X, S))

Proof of Theorem nchoicelem10

Dummy variables y t z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nchoicelem10.2	. 2 |- X e. _V
2		elrn 4897	. . . . 5 |- (<.{y}, X>. e. ran (`' ∼ S (x) (`' S |` Fix( S o. ImageS))) <-> E.z z(`' ∼ S (x) (`' S |` Fix( S o. ImageS)))<.{y}, X>.)
3		trtxp 5782	. . . . . . 7 |- (z(`' ∼ S (x) (`' S |` Fix( S o. ImageS)))<.{y}, X>. <-> (z`' ∼ S {y} /\ z(`' S |` Fix( S o. ImageS))X))
4		brcnv 4893	. . . . . . . . . 10 |- (z`' ∼ S {y} <-> {y} ∼ S z)
5		df-br 4641	. . . . . . . . . 10 |- ({y} ∼ S z <-> <.{y}, z>. e. ∼ S )
6		snex 4112	. . . . . . . . . . . . 13 |- {y} e. _V
7		vex 2863	. . . . . . . . . . . . 13 |- z e. _V
8	6, 7	opex 4589	. . . . . . . . . . . 12 |- <.{y}, z>. e. _V
9	8	elcompl 3226	. . . . . . . . . . 11 |- (<.{y}, z>. e. ∼ S <-> -. <.{y}, z>. e. S )
10		vex 2863	. . . . . . . . . . . 12 |- y e. _V
11	10, 7	opelssetsn 4761	. . . . . . . . . . 11 |- (<.{y}, z>. e. S <-> y e. z)
12	9, 11	xchbinx 301	. . . . . . . . . 10 |- (<.{y}, z>. e. ∼ S <-> -. y e. z)
13	4, 5, 12	3bitri 262	. . . . . . . . 9 |- (z`' ∼ S {y} <-> -. y e. z)
14		brres 4950	. . . . . . . . . 10 |- (z(`' S |` Fix( S o. ImageS))X <-> (z`' S X /\ z e. Fix( S o. ImageS)))
15		brcnv 4893	. . . . . . . . . . . 12 |- (z`' S X <-> X S z)
16	1, 7	brsset 4759	. . . . . . . . . . . 12 |- (X S z <-> X C_ z)
17	15, 16	bitri 240	. . . . . . . . . . 11 |- (z`' S X <-> X C_ z)
18		elfix 5788	. . . . . . . . . . . 12 |- (z e. Fix( S o. ImageS) <-> z( S o. ImageS)z)
19		brco 4884	. . . . . . . . . . . . 13 |- (z( S o. ImageS)z <-> E.t(zImageSt /\ t S z))
20		vex 2863	. . . . . . . . . . . . . . . 16 |- t e. _V
21	7, 20	brimage 5794	. . . . . . . . . . . . . . 15 |- (zImageSt <-> t = (S"z))
22	20, 7	brsset 4759	. . . . . . . . . . . . . . 15 |- (t S z <-> t C_ z)
23	21, 22	anbi12i 678	. . . . . . . . . . . . . 14 |- ((zImageSt /\ t S z) <-> (t = (S"z) /\ t C_ z))
24	23	exbii 1582	. . . . . . . . . . . . 13 |- (E.t(zImageSt /\ t S z) <-> E.t(t = (S"z) /\ t C_ z))
25		nchoicelem10.1	. . . . . . . . . . . . . . 15 |- S e. _V
26	25, 7	imaex 4748	. . . . . . . . . . . . . 14 |- (S"z) e. _V
27		sseq1 3293	. . . . . . . . . . . . . 14 |- (t = (S"z) -> (t C_ z <-> (S"z) C_ z))
28	26, 27	ceqsexv 2895	. . . . . . . . . . . . 13 |- (E.t(t = (S"z) /\ t C_ z) <-> (S"z) C_ z)
29	19, 24, 28	3bitri 262	. . . . . . . . . . . 12 |- (z( S o. ImageS)z <-> (S"z) C_ z)
30	18, 29	bitri 240	. . . . . . . . . . 11 |- (z e. Fix( S o. ImageS) <-> (S"z) C_ z)
31	17, 30	anbi12i 678	. . . . . . . . . 10 |- ((z`' S X /\ z e. Fix( S o. ImageS)) <-> (X C_ z /\ (S"z) C_ z))
32	14, 31	bitri 240	. . . . . . . . 9 |- (z(`' S |` Fix( S o. ImageS))X <-> (X C_ z /\ (S"z) C_ z))
33	13, 32	anbi12i 678	. . . . . . . 8 |- ((z`' ∼ S {y} /\ z(`' S |` Fix( S o. ImageS))X) <-> (-. y e. z /\ (X C_ z /\ (S"z) C_ z)))
34		ancom 437	. . . . . . . 8 |- ((-. y e. z /\ (X C_ z /\ (S"z) C_ z)) <-> ((X C_ z /\ (S"z) C_ z) /\ -. y e. z))
35	33, 34	bitri 240	. . . . . . 7 |- ((z`' ∼ S {y} /\ z(`' S |` Fix( S o. ImageS))X) <-> ((X C_ z /\ (S"z) C_ z) /\ -. y e. z))
36		annim 414	. . . . . . 7 |- (((X C_ z /\ (S"z) C_ z) /\ -. y e. z) <-> -. ((X C_ z /\ (S"z) C_ z) -> y e. z))
37	3, 35, 36	3bitri 262	. . . . . 6 |- (z(`' ∼ S (x) (`' S |` Fix( S o. ImageS)))<.{y}, X>. <-> -. ((X C_ z /\ (S"z) C_ z) -> y e. z))
38	37	exbii 1582	. . . . 5 |- (E.z z(`' ∼ S (x) (`' S |` Fix( S o. ImageS)))<.{y}, X>. <-> E.z -. ((X C_ z /\ (S"z) C_ z) -> y e. z))
39		exnal 1574	. . . . 5 |- (E.z -. ((X C_ z /\ (S"z) C_ z) -> y e. z) <-> -. A.z((X C_ z /\ (S"z) C_ z) -> y e. z))
40	2, 38, 39	3bitrri 263	. . . 4 |- (-. A.z((X C_ z /\ (S"z) C_ z) -> y e. z) <-> <.{y}, X>. e. ran (`' ∼ S (x) (`' S |` Fix( S o. ImageS))))
41	40	con1bii 321	. . 3 |- (-. <.{y}, X>. e. ran (`' ∼ S (x) (`' S |` Fix( S o. ImageS))) <-> A.z((X C_ z /\ (S"z) C_ z) -> y e. z))
42	6, 1	opex 4589	. . . 4 |- <.{y}, X>. e. _V
43	42	elcompl 3226	. . 3 |- (<.{y}, X>. e. ∼ ran (`' ∼ S (x) (`' S |` Fix( S o. ImageS))) <-> -. <.{y}, X>. e. ran (`' ∼ S (x) (`' S |` Fix( S o. ImageS))))
44		df-clos1 5874	. . . . 5 |- Clos1 (X, S) = |^|{z | (X C_ z /\ (S"z) C_ z)}
45	44	eleq2i 2417	. . . 4 |- (y e. Clos1 (X, S) <-> y e. |^|{z | (X C_ z /\ (S"z) C_ z)})
46	10	elintab 3938	. . . 4 |- (y e. |^|{z | (X C_ z /\ (S"z) C_ z)} <-> A.z((X C_ z /\ (S"z) C_ z) -> y e. z))
47	45, 46	bitri 240	. . 3 |- (y e. Clos1 (X, S) <-> A.z((X C_ z /\ (S"z) C_ z) -> y e. z))
48	41, 43, 47	3bitr4i 268	. 2 |- (<.{y}, X>. e. ∼ ran (`' ∼ S (x) (`' S |` Fix( S o. ImageS))) <-> y e. Clos1 (X, S))
49	1, 48	releqel 5808	1 |- (<.c, X>. e. ∼ (( Ins3 S (+) Ins2 ∼ ran (`' ∼ S (x) (`' S |` Fix( S o. ImageS))))"1c) <-> c = Clos1 (X, S))

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176   /\ wa 358  A.wal 1540  E.wex 1541   = wceq 1642   e. wcel 1710  {cab 2339  _Vcvv 2860   ∼ ccompl 3206   (+) csymdif 3210   C_ wss 3258  {csn 3738  |^|cint 3927  1_cc1c 4135  <.cop 4562   class class class wbr 4640   S csset 4720   o. ccom 4722  "cima 4723  `'ccnv 4772  ran crn 4774   |` cres 4775   (x) ctxp 5736  Fixcfix 5740   Ins2 cins2 5750   Ins3 cins3 5752  Imagecimage 5754   Clos1 cclos1 5873

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-sset 4726  df-co 4727  df-ima 4728  df-si 4729  df-id 4768  df-xp 4785  df-cnv 4786  df-rn 4787  df-res 4789  df-2nd 4798  df-txp 5737  df-fix 5741  df-ins2 5751  df-ins3 5753  df-image 5755  df-clos1 5874

This theorem is referenced by:  nchoicelem11  6300  nchoicelem16  6305  nchoicelem18  6307