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

Theorem nchoicelem10 6298
 Description: Lemma for nchoice 6308. 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.
StepHypRef Expression
1 nchoicelem10.2 . 2 X V
2 elrn 4896 . . . . 5 ({y}, X ran ( S ⊗ ( S Fix ( S ImageS))) ↔ z z( S ⊗ ( S Fix ( S ImageS))){y}, X)
3 trtxp 5781 . . . . . . 7 (z( S ⊗ ( S Fix ( S ImageS))){y}, X ↔ (z S {y} z( S Fix ( S ImageS))X))
4 brcnv 4892 . . . . . . . . . 10 (z S {y} ↔ {y} ∼ S z)
5 df-br 4640 . . . . . . . . . 10 ({y} ∼ S z{y}, z S )
6 snex 4111 . . . . . . . . . . . . 13 {y} V
7 vex 2862 . . . . . . . . . . . . 13 z V
86, 7opex 4588 . . . . . . . . . . . 12 {y}, z V
98elcompl 3225 . . . . . . . . . . 11 ({y}, z S ↔ ¬ {y}, z S )
10 vex 2862 . . . . . . . . . . . 12 y V
1110, 7opelssetsn 4760 . . . . . . . . . . 11 ({y}, z S y z)
129, 11xchbinx 301 . . . . . . . . . 10 ({y}, z S ↔ ¬ y z)
134, 5, 123bitri 262 . . . . . . . . 9 (z S {y} ↔ ¬ y z)
14 brres 4949 . . . . . . . . . 10 (z( S Fix ( S ImageS))X ↔ (z S X z Fix ( S ImageS)))
15 brcnv 4892 . . . . . . . . . . . 12 (z S XX S z)
161, 7brsset 4758 . . . . . . . . . . . 12 (X S zX z)
1715, 16bitri 240 . . . . . . . . . . 11 (z S XX z)
18 elfix 5787 . . . . . . . . . . . 12 (z Fix ( S ImageS) ↔ z( S ImageS)z)
19 brco 4883 . . . . . . . . . . . . 13 (z( S ImageS)zt(zImageSt t S z))
20 vex 2862 . . . . . . . . . . . . . . . 16 t V
217, 20brimage 5793 . . . . . . . . . . . . . . 15 (zImageStt = (Sz))
2220, 7brsset 4758 . . . . . . . . . . . . . . 15 (t S zt z)
2321, 22anbi12i 678 . . . . . . . . . . . . . 14 ((zImageSt t S z) ↔ (t = (Sz) t z))
2423exbii 1582 . . . . . . . . . . . . 13 (t(zImageSt t S z) ↔ t(t = (Sz) t z))
25 nchoicelem10.1 . . . . . . . . . . . . . . 15 S V
2625, 7imaex 4747 . . . . . . . . . . . . . 14 (Sz) V
27 sseq1 3292 . . . . . . . . . . . . . 14 (t = (Sz) → (t z ↔ (Sz) z))
2826, 27ceqsexv 2894 . . . . . . . . . . . . 13 (t(t = (Sz) t z) ↔ (Sz) z)
2919, 24, 283bitri 262 . . . . . . . . . . . 12 (z( S ImageS)z ↔ (Sz) z)
3018, 29bitri 240 . . . . . . . . . . 11 (z Fix ( S ImageS) ↔ (Sz) z)
3117, 30anbi12i 678 . . . . . . . . . 10 ((z S X z Fix ( S ImageS)) ↔ (X z (Sz) z))
3214, 31bitri 240 . . . . . . . . 9 (z( S Fix ( S ImageS))X ↔ (X z (Sz) z))
3313, 32anbi12i 678 . . . . . . . 8 ((z S {y} z( S Fix ( S ImageS))X) ↔ (¬ y z (X z (Sz) z)))
34 ancom 437 . . . . . . . 8 ((¬ y z (X z (Sz) z)) ↔ ((X z (Sz) z) ¬ y z))
3533, 34bitri 240 . . . . . . 7 ((z S {y} z( S Fix ( S ImageS))X) ↔ ((X z (Sz) z) ¬ y z))
36 annim 414 . . . . . . 7 (((X z (Sz) z) ¬ y z) ↔ ¬ ((X z (Sz) z) → y z))
373, 35, 363bitri 262 . . . . . 6 (z( S ⊗ ( S Fix ( S ImageS))){y}, X ↔ ¬ ((X z (Sz) z) → y z))
3837exbii 1582 . . . . 5 (z z( S ⊗ ( S Fix ( S ImageS))){y}, Xz ¬ ((X z (Sz) z) → y z))
39 exnal 1574 . . . . 5 (z ¬ ((X z (Sz) z) → y z) ↔ ¬ z((X z (Sz) z) → y z))
402, 38, 393bitrri 263 . . . 4 z((X z (Sz) z) → y z) ↔ {y}, X ran ( S ⊗ ( S Fix ( S ImageS))))
4140con1bii 321 . . 3 {y}, X ran ( S ⊗ ( S Fix ( S ImageS))) ↔ z((X z (Sz) z) → y z))
426, 1opex 4588 . . . 4 {y}, X V
4342elcompl 3225 . . 3 ({y}, X ∼ ran ( S ⊗ ( S Fix ( S ImageS))) ↔ ¬ {y}, X ran ( S ⊗ ( S Fix ( S ImageS))))
44 df-clos1 5873 . . . . 5 Clos1 (X, S) = {z (X z (Sz) z)}
4544eleq2i 2417 . . . 4 (y Clos1 (X, S) ↔ y {z (X z (Sz) z)})
4610elintab 3937 . . . 4 (y {z (X z (Sz) z)} ↔ z((X z (Sz) z) → y z))
4745, 46bitri 240 . . 3 (y Clos1 (X, S) ↔ z((X z (Sz) z) → y z))
4841, 43, 473bitr4i 268 . 2 ({y}, X ∼ ran ( S ⊗ ( S Fix ( S ImageS))) ↔ y Clos1 (X, S))
491, 48releqel 5807 1 (c, X ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S ImageS)))) “ 1c) ↔ c = Clos1 (X, S))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710  {cab 2339  Vcvv 2859   ∼ ccompl 3205   ⊕ csymdif 3209   ⊆ wss 3257  {csn 3737  ∩cint 3926  1cc1c 4134  ⟨cop 4561   class class class wbr 4639   S csset 4719   ∘ ccom 4721   “ cima 4722  ◡ccnv 4771  ran crn 4773   ↾ cres 4774   ⊗ ctxp 5735   Fix cfix 5739   Ins2 cins2 5749   Ins3 cins3 5751  Imagecimage 5753   Clos1 cclos1 5872 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-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
 Copyright terms: Public domain W3C validator