Theorem nchoicelem10 6298

Description: Lemma for nchoice 6308. 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 4896	. . . . 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 5781	. . . . . . 7 |- (z(`' ∼ S (x) (`' S |` Fix( S o. ImageS)))<.{y}, X>. <-> (z`' ∼ S {y} /\ z(`' S |` Fix( S o. ImageS))X))
4		brcnv 4892	. . . . . . . . . 10 |- (z`' ∼ S {y} <-> {y} ∼ S z)
5		df-br 4640	. . . . . . . . . 10 |- ({y} ∼ S z <-> <.{y}, z>. e. ∼ S )
6		snex 4111	. . . . . . . . . . . . 13 |- {y} e. _V
7		vex 2862	. . . . . . . . . . . . 13 |- z e. _V
8	6, 7	opex 4588	. . . . . . . . . . . 12 |- <.{y}, z>. e. _V
9	8	elcompl 3225	. . . . . . . . . . 11 |- (<.{y}, z>. e. ∼ S <-> -. <.{y}, z>. e. S )
10		vex 2862	. . . . . . . . . . . 12 |- y e. _V
11	10, 7	opelssetsn 4760	. . . . . . . . . . 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 4949	. . . . . . . . . 10 |- (z(`' S |` Fix( S o. ImageS))X <-> (z`' S X /\ z e. Fix( S o. ImageS)))
15		brcnv 4892	. . . . . . . . . . . 12 |- (z`' S X <-> X S z)
16	1, 7	brsset 4758	. . . . . . . . . . . 12 |- (X S z <-> X C_ z)
17	15, 16	bitri 240	. . . . . . . . . . 11 |- (z`' S X <-> X C_ z)
18		elfix 5787	. . . . . . . . . . . 12 |- (z e. Fix( S o. ImageS) <-> z( S o. ImageS)z)
19		brco 4883	. . . . . . . . . . . . 13 |- (z( S o. ImageS)z <-> E.t(zImageSt /\ t S z))
20		vex 2862	. . . . . . . . . . . . . . . 16 |- t e. _V
21	7, 20	brimage 5793	. . . . . . . . . . . . . . 15 |- (zImageSt <-> t = (S"z))
22	20, 7	brsset 4758	. . . . . . . . . . . . . . 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 4747	. . . . . . . . . . . . . 14 |- (S"z) e. _V
27		sseq1 3292	. . . . . . . . . . . . . 14 |- (t = (S"z) -> (t C_ z <-> (S"z) C_ z))
28	26, 27	ceqsexv 2894	. . . . . . . . . . . . 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 4588	. . . 4 |- <.{y}, X>. e. _V
43	42	elcompl 3225	. . 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 5873	. . . . 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 3937	. . . 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 5807	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 2859   ∼ ccompl 3205   (+) csymdif 3209   C_ wss 3257  {csn 3737  |^|cint 3926  1_cc1c 4134  <.cop 4561   class class class wbr 4639   S csset 4719   o. ccom 4721  "cima 4722  `'ccnv 4771  ran crn 4773   |` cres 4774   (x) ctxp 5735  Fixcfix 5739   Ins2 cins2 5749   Ins3 cins3 5751  Imagecimage 5753   Clos1 cclos1 5872

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-sset 4725  df-co 4726  df-ima 4727  df-si 4728  df-id 4767  df-xp 4784  df-cnv 4785  df-rn 4786  df-res 4788  df-2nd 4797  df-txp 5736  df-fix 5740  df-ins2 5750  df-ins3 5752  df-image 5754  df-clos1 5873

This theorem is referenced by:  nchoicelem11  6299  nchoicelem16  6304  nchoicelem18  6306