Theorem nchoicelem10 6299

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

Hypotheses

Ref	Expression
nchoicelem10.1	⊢ S ∈ V
nchoicelem10.2	⊢ X ∈ V

Assertion

Ref	Expression
nchoicelem10	⊢ (⟨c, X⟩ ∈ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ 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 ∈ V
2		elrn 4897	. . . . 5 ⊢ (⟨{y}, X⟩ ∈ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ ImageS))) ↔ ∃z z(◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ ImageS)))⟨{y}, X⟩)
3		trtxp 5782	. . . . . . 7 ⊢ (z(◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ ImageS)))⟨{y}, X⟩ ↔ (z◡ ∼ S {y} ∧ z(◡ S ↾ Fix ( S ∘ ImageS))X))
4		brcnv 4893	. . . . . . . . . 10 ⊢ (z◡ ∼ S {y} ↔ {y} ∼ S z)
5		df-br 4641	. . . . . . . . . 10 ⊢ ({y} ∼ S z ↔ ⟨{y}, z⟩ ∈ ∼ S )
6		snex 4112	. . . . . . . . . . . . 13 ⊢ {y} ∈ V
7		vex 2863	. . . . . . . . . . . . 13 ⊢ z ∈ V
8	6, 7	opex 4589	. . . . . . . . . . . 12 ⊢ ⟨{y}, z⟩ ∈ V
9	8	elcompl 3226	. . . . . . . . . . 11 ⊢ (⟨{y}, z⟩ ∈ ∼ S ↔ ¬ ⟨{y}, z⟩ ∈ S )
10		vex 2863	. . . . . . . . . . . 12 ⊢ y ∈ V
11	10, 7	opelssetsn 4761	. . . . . . . . . . 11 ⊢ (⟨{y}, z⟩ ∈ S ↔ y ∈ z)
12	9, 11	xchbinx 301	. . . . . . . . . 10 ⊢ (⟨{y}, z⟩ ∈ ∼ S ↔ ¬ y ∈ z)
13	4, 5, 12	3bitri 262	. . . . . . . . 9 ⊢ (z◡ ∼ S {y} ↔ ¬ y ∈ z)
14		brres 4950	. . . . . . . . . 10 ⊢ (z(◡ S ↾ Fix ( S ∘ ImageS))X ↔ (z◡ S X ∧ z ∈ Fix ( S ∘ ImageS)))
15		brcnv 4893	. . . . . . . . . . . 12 ⊢ (z◡ S X ↔ X S z)
16	1, 7	brsset 4759	. . . . . . . . . . . 12 ⊢ (X S z ↔ X ⊆ z)
17	15, 16	bitri 240	. . . . . . . . . . 11 ⊢ (z◡ S X ↔ X ⊆ z)
18		elfix 5788	. . . . . . . . . . . 12 ⊢ (z ∈ Fix ( S ∘ ImageS) ↔ z( S ∘ ImageS)z)
19		brco 4884	. . . . . . . . . . . . 13 ⊢ (z( S ∘ ImageS)z ↔ ∃t(zImageSt ∧ t S z))
20		vex 2863	. . . . . . . . . . . . . . . 16 ⊢ t ∈ V
21	7, 20	brimage 5794	. . . . . . . . . . . . . . 15 ⊢ (zImageSt ↔ t = (S “ z))
22	20, 7	brsset 4759	. . . . . . . . . . . . . . 15 ⊢ (t S z ↔ t ⊆ z)
23	21, 22	anbi12i 678	. . . . . . . . . . . . . 14 ⊢ ((zImageSt ∧ t S z) ↔ (t = (S “ z) ∧ t ⊆ z))
24	23	exbii 1582	. . . . . . . . . . . . 13 ⊢ (∃t(zImageSt ∧ t S z) ↔ ∃t(t = (S “ z) ∧ t ⊆ z))
25		nchoicelem10.1	. . . . . . . . . . . . . . 15 ⊢ S ∈ V
26	25, 7	imaex 4748	. . . . . . . . . . . . . 14 ⊢ (S “ z) ∈ V
27		sseq1 3293	. . . . . . . . . . . . . 14 ⊢ (t = (S “ z) → (t ⊆ z ↔ (S “ z) ⊆ z))
28	26, 27	ceqsexv 2895	. . . . . . . . . . . . 13 ⊢ (∃t(t = (S “ z) ∧ t ⊆ z) ↔ (S “ z) ⊆ z)
29	19, 24, 28	3bitri 262	. . . . . . . . . . . 12 ⊢ (z( S ∘ ImageS)z ↔ (S “ z) ⊆ z)
30	18, 29	bitri 240	. . . . . . . . . . 11 ⊢ (z ∈ Fix ( S ∘ ImageS) ↔ (S “ z) ⊆ z)
31	17, 30	anbi12i 678	. . . . . . . . . 10 ⊢ ((z◡ S X ∧ z ∈ Fix ( S ∘ ImageS)) ↔ (X ⊆ z ∧ (S “ z) ⊆ z))
32	14, 31	bitri 240	. . . . . . . . 9 ⊢ (z(◡ S ↾ Fix ( S ∘ ImageS))X ↔ (X ⊆ z ∧ (S “ z) ⊆ z))
33	13, 32	anbi12i 678	. . . . . . . 8 ⊢ ((z◡ ∼ S {y} ∧ z(◡ S ↾ Fix ( S ∘ ImageS))X) ↔ (¬ y ∈ z ∧ (X ⊆ z ∧ (S “ z) ⊆ z)))
34		ancom 437	. . . . . . . 8 ⊢ ((¬ y ∈ z ∧ (X ⊆ z ∧ (S “ z) ⊆ z)) ↔ ((X ⊆ z ∧ (S “ z) ⊆ z) ∧ ¬ y ∈ z))
35	33, 34	bitri 240	. . . . . . 7 ⊢ ((z◡ ∼ S {y} ∧ z(◡ S ↾ Fix ( S ∘ ImageS))X) ↔ ((X ⊆ z ∧ (S “ z) ⊆ z) ∧ ¬ y ∈ z))
36		annim 414	. . . . . . 7 ⊢ (((X ⊆ z ∧ (S “ z) ⊆ z) ∧ ¬ y ∈ z) ↔ ¬ ((X ⊆ z ∧ (S “ z) ⊆ z) → y ∈ z))
37	3, 35, 36	3bitri 262	. . . . . 6 ⊢ (z(◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ ImageS)))⟨{y}, X⟩ ↔ ¬ ((X ⊆ z ∧ (S “ z) ⊆ z) → y ∈ z))
38	37	exbii 1582	. . . . 5 ⊢ (∃z z(◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ ImageS)))⟨{y}, X⟩ ↔ ∃z ¬ ((X ⊆ z ∧ (S “ z) ⊆ z) → y ∈ z))
39		exnal 1574	. . . . 5 ⊢ (∃z ¬ ((X ⊆ z ∧ (S “ z) ⊆ z) → y ∈ z) ↔ ¬ ∀z((X ⊆ z ∧ (S “ z) ⊆ z) → y ∈ z))
40	2, 38, 39	3bitrri 263	. . . 4 ⊢ (¬ ∀z((X ⊆ z ∧ (S “ z) ⊆ z) → y ∈ z) ↔ ⟨{y}, X⟩ ∈ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ ImageS))))
41	40	con1bii 321	. . 3 ⊢ (¬ ⟨{y}, X⟩ ∈ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ ImageS))) ↔ ∀z((X ⊆ z ∧ (S “ z) ⊆ z) → y ∈ z))
42	6, 1	opex 4589	. . . 4 ⊢ ⟨{y}, X⟩ ∈ V
43	42	elcompl 3226	. . 3 ⊢ (⟨{y}, X⟩ ∈ ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ ImageS))) ↔ ¬ ⟨{y}, X⟩ ∈ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ ImageS))))
44		df-clos1 5874	. . . . 5 ⊢ Clos1 (X, S) = ∩{z ∣ (X ⊆ z ∧ (S “ z) ⊆ z)}
45	44	eleq2i 2417	. . . 4 ⊢ (y ∈ Clos1 (X, S) ↔ y ∈ ∩{z ∣ (X ⊆ z ∧ (S “ z) ⊆ z)})
46	10	elintab 3938	. . . 4 ⊢ (y ∈ ∩{z ∣ (X ⊆ z ∧ (S “ z) ⊆ z)} ↔ ∀z((X ⊆ z ∧ (S “ z) ⊆ z) → y ∈ z))
47	45, 46	bitri 240	. . 3 ⊢ (y ∈ Clos1 (X, S) ↔ ∀z((X ⊆ z ∧ (S “ z) ⊆ z) → y ∈ z))
48	41, 43, 47	3bitr4i 268	. 2 ⊢ (⟨{y}, X⟩ ∈ ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ ImageS))) ↔ y ∈ Clos1 (X, S))
49	1, 48	releqel 5808	1 ⊢ (⟨c, X⟩ ∈ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ ImageS)))) “ 1c) ↔ c = Clos1 (X, S))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710  {cab 2339  Vcvv 2860   ∼ ccompl 3206   ⊕ csymdif 3210   ⊆ wss 3258  {csn 3738  ∩cint 3927  1_cc1c 4135  ⟨cop 4562   class class class wbr 4640   S csset 4720   ∘ ccom 4722   “ cima 4723  ^◡ccnv 4772  ran crn 4774   ↾ cres 4775   ⊗ ctxp 5736   Fix cfix 5740   Ins2 cins2 5750   Ins3 cins3 5752  Imagecimage 5754   Clos1 cclos1 5873

This proof depends on 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 proof 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 used by:  nchoicelem11  6300  nchoicelem16  6305  nchoicelem18  6307