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

Theorem spacind 6287
Description: Inductive law for the special set generator. (Contributed by SF, 13-Mar-2015.)
Assertion
Ref Expression
spacind (((M NC S V) (M S x ( SpacM)((x S (xc 0c) NC ) → (2cc x) S))) → ( SpacM) S)
Distinct variable groups:   x,M   x,S
Allowed substitution hint:   V(x)

Proof of Theorem spacind
Dummy variables z q p are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 2867 . 2 (S VS V)
2 spacval 6282 . . . . 5 (M NC → ( SpacM) = Clos1 ({M}, {p, q (p NC q NC q = (2cc p))}))
32adantr 451 . . . 4 ((M NC S V) → ( SpacM) = Clos1 ({M}, {p, q (p NC q NC q = (2cc p))}))
43adantr 451 . . 3 (((M NC S V) (M S x ( SpacM)((x S (xc 0c) NC ) → (2cc x) S))) → ( SpacM) = Clos1 ({M}, {p, q (p NC q NC q = (2cc p))}))
5 simplr 731 . . . 4 (((M NC S V) (M S x ( SpacM)((x S (xc 0c) NC ) → (2cc x) S))) → S V)
6 snssi 3852 . . . . . 6 (M S → {M} S)
76adantr 451 . . . . 5 ((M S x ( SpacM)((x S (xc 0c) NC ) → (2cc x) S)) → {M} S)
87adantl 452 . . . 4 (((M NC S V) (M S x ( SpacM)((x S (xc 0c) NC ) → (2cc x) S))) → {M} S)
9 spacssnc 6284 . . . . . . . . . . 11 (M NC → ( SpacM) NC )
109sseld 3272 . . . . . . . . . 10 (M NC → (x ( SpacM) → x NC ))
11 2nc 6168 . . . . . . . . . . . . . . . . . . . 20 2c NC
12 ceclr 6187 . . . . . . . . . . . . . . . . . . . . 21 ((2c NC x NC (2cc x) NC ) → ((2cc 0c) NC (xc 0c) NC ))
1312simprd 449 . . . . . . . . . . . . . . . . . . . 20 ((2c NC x NC (2cc x) NC ) → (xc 0c) NC )
1411, 13mp3an1 1264 . . . . . . . . . . . . . . . . . . 19 ((x NC (2cc x) NC ) → (xc 0c) NC )
1514ex 423 . . . . . . . . . . . . . . . . . 18 (x NC → ((2cc x) NC → (xc 0c) NC ))
1615imim1d 69 . . . . . . . . . . . . . . . . 17 (x NC → (((xc 0c) NC → (2cc x) S) → ((2cc x) NC → (2cc x) S)))
1716a1dd 42 . . . . . . . . . . . . . . . 16 (x NC → (((xc 0c) NC → (2cc x) S) → (x NC → ((2cc x) NC → (2cc x) S))))
1817adantl 452 . . . . . . . . . . . . . . 15 ((M NC x NC ) → (((xc 0c) NC → (2cc x) S) → (x NC → ((2cc x) NC → (2cc x) S))))
19 3anass 938 . . . . . . . . . . . . . . . . . . 19 ((x NC z NC z = (2cc x)) ↔ (x NC (z NC z = (2cc x))))
2019imbi1i 315 . . . . . . . . . . . . . . . . . 18 (((x NC z NC z = (2cc x)) → z S) ↔ ((x NC (z NC z = (2cc x))) → z S))
21 impexp 433 . . . . . . . . . . . . . . . . . 18 (((x NC (z NC z = (2cc x))) → z S) ↔ (x NC → ((z NC z = (2cc x)) → z S)))
2220, 21bitri 240 . . . . . . . . . . . . . . . . 17 (((x NC z NC z = (2cc x)) → z S) ↔ (x NC → ((z NC z = (2cc x)) → z S)))
2322albii 1566 . . . . . . . . . . . . . . . 16 (z((x NC z NC z = (2cc x)) → z S) ↔ z(x NC → ((z NC z = (2cc x)) → z S)))
24 19.21v 1890 . . . . . . . . . . . . . . . . 17 (z(x NC → ((z NC z = (2cc x)) → z S)) ↔ (x NCz((z NC z = (2cc x)) → z S)))
25 impexp 433 . . . . . . . . . . . . . . . . . . . . 21 (((z NC z = (2cc x)) → z S) ↔ (z NC → (z = (2cc x) → z S)))
26 bi2.04 350 . . . . . . . . . . . . . . . . . . . . 21 ((z NC → (z = (2cc x) → z S)) ↔ (z = (2cc x) → (z NCz S)))
2725, 26bitri 240 . . . . . . . . . . . . . . . . . . . 20 (((z NC z = (2cc x)) → z S) ↔ (z = (2cc x) → (z NCz S)))
2827albii 1566 . . . . . . . . . . . . . . . . . . 19 (z((z NC z = (2cc x)) → z S) ↔ z(z = (2cc x) → (z NCz S)))
29 ovex 5551 . . . . . . . . . . . . . . . . . . . 20 (2cc x) V
30 eleq1 2413 . . . . . . . . . . . . . . . . . . . . 21 (z = (2cc x) → (z NC ↔ (2cc x) NC ))
31 eleq1 2413 . . . . . . . . . . . . . . . . . . . . 21 (z = (2cc x) → (z S ↔ (2cc x) S))
3230, 31imbi12d 311 . . . . . . . . . . . . . . . . . . . 20 (z = (2cc x) → ((z NCz S) ↔ ((2cc x) NC → (2cc x) S)))
3329, 32ceqsalv 2885 . . . . . . . . . . . . . . . . . . 19 (z(z = (2cc x) → (z NCz S)) ↔ ((2cc x) NC → (2cc x) S))
3428, 33bitri 240 . . . . . . . . . . . . . . . . . 18 (z((z NC z = (2cc x)) → z S) ↔ ((2cc x) NC → (2cc x) S))
3534imbi2i 303 . . . . . . . . . . . . . . . . 17 ((x NCz((z NC z = (2cc x)) → z S)) ↔ (x NC → ((2cc x) NC → (2cc x) S)))
3624, 35bitri 240 . . . . . . . . . . . . . . . 16 (z(x NC → ((z NC z = (2cc x)) → z S)) ↔ (x NC → ((2cc x) NC → (2cc x) S)))
3723, 36bitri 240 . . . . . . . . . . . . . . 15 (z((x NC z NC z = (2cc x)) → z S) ↔ (x NC → ((2cc x) NC → (2cc x) S)))
3818, 37syl6ibr 218 . . . . . . . . . . . . . 14 ((M NC x NC ) → (((xc 0c) NC → (2cc x) S) → z((x NC z NC z = (2cc x)) → z S)))
39 vex 2862 . . . . . . . . . . . . . . . . 17 x V
40 vex 2862 . . . . . . . . . . . . . . . . 17 z V
41 eleq1 2413 . . . . . . . . . . . . . . . . . 18 (p = x → (p NCx NC ))
42 oveq2 5531 . . . . . . . . . . . . . . . . . . 19 (p = x → (2cc p) = (2cc x))
4342eqeq2d 2364 . . . . . . . . . . . . . . . . . 18 (p = x → (q = (2cc p) ↔ q = (2cc x)))
4441, 433anbi13d 1254 . . . . . . . . . . . . . . . . 17 (p = x → ((p NC q NC q = (2cc p)) ↔ (x NC q NC q = (2cc x))))
45 eleq1 2413 . . . . . . . . . . . . . . . . . 18 (q = z → (q NCz NC ))
46 eqeq1 2359 . . . . . . . . . . . . . . . . . 18 (q = z → (q = (2cc x) ↔ z = (2cc x)))
4745, 463anbi23d 1255 . . . . . . . . . . . . . . . . 17 (q = z → ((x NC q NC q = (2cc x)) ↔ (x NC z NC z = (2cc x))))
48 eqid 2353 . . . . . . . . . . . . . . . . 17 {p, q (p NC q NC q = (2cc p))} = {p, q (p NC q NC q = (2cc p))}
4939, 40, 44, 47, 48brab 4709 . . . . . . . . . . . . . . . 16 (x{p, q (p NC q NC q = (2cc p))}z ↔ (x NC z NC z = (2cc x)))
5049imbi1i 315 . . . . . . . . . . . . . . 15 ((x{p, q (p NC q NC q = (2cc p))}zz S) ↔ ((x NC z NC z = (2cc x)) → z S))
5150albii 1566 . . . . . . . . . . . . . 14 (z(x{p, q (p NC q NC q = (2cc p))}zz S) ↔ z((x NC z NC z = (2cc x)) → z S))
5238, 51syl6ibr 218 . . . . . . . . . . . . 13 ((M NC x NC ) → (((xc 0c) NC → (2cc x) S) → z(x{p, q (p NC q NC q = (2cc p))}zz S)))
5352imim2d 48 . . . . . . . . . . . 12 ((M NC x NC ) → ((x S → ((xc 0c) NC → (2cc x) S)) → (x Sz(x{p, q (p NC q NC q = (2cc p))}zz S))))
54 impexp 433 . . . . . . . . . . . 12 (((x S (xc 0c) NC ) → (2cc x) S) ↔ (x S → ((xc 0c) NC → (2cc x) S)))
55 impexp 433 . . . . . . . . . . . . . 14 (((x S x{p, q (p NC q NC q = (2cc p))}z) → z S) ↔ (x S → (x{p, q (p NC q NC q = (2cc p))}zz S)))
5655albii 1566 . . . . . . . . . . . . 13 (z((x S x{p, q (p NC q NC q = (2cc p))}z) → z S) ↔ z(x S → (x{p, q (p NC q NC q = (2cc p))}zz S)))
57 19.21v 1890 . . . . . . . . . . . . 13 (z(x S → (x{p, q (p NC q NC q = (2cc p))}zz S)) ↔ (x Sz(x{p, q (p NC q NC q = (2cc p))}zz S)))
5856, 57bitri 240 . . . . . . . . . . . 12 (z((x S x{p, q (p NC q NC q = (2cc p))}z) → z S) ↔ (x Sz(x{p, q (p NC q NC q = (2cc p))}zz S)))
5953, 54, 583imtr4g 261 . . . . . . . . . . 11 ((M NC x NC ) → (((x S (xc 0c) NC ) → (2cc x) S) → z((x S x{p, q (p NC q NC q = (2cc p))}z) → z S)))
6059ex 423 . . . . . . . . . 10 (M NC → (x NC → (((x S (xc 0c) NC ) → (2cc x) S) → z((x S x{p, q (p NC q NC q = (2cc p))}z) → z S))))
6110, 60syld 40 . . . . . . . . 9 (M NC → (x ( SpacM) → (((x S (xc 0c) NC ) → (2cc x) S) → z((x S x{p, q (p NC q NC q = (2cc p))}z) → z S))))
6261imp 418 . . . . . . . 8 ((M NC x ( SpacM)) → (((x S (xc 0c) NC ) → (2cc x) S) → z((x S x{p, q (p NC q NC q = (2cc p))}z) → z S)))
6362ralimdva 2692 . . . . . . 7 (M NC → (x ( SpacM)((x S (xc 0c) NC ) → (2cc x) S) → x ( SpacM)z((x S x{p, q (p NC q NC q = (2cc p))}z) → z S)))
64 raleq 2807 . . . . . . . 8 (( SpacM) = Clos1 ({M}, {p, q (p NC q NC q = (2cc p))}) → (x ( SpacM)z((x S x{p, q (p NC q NC q = (2cc p))}z) → z S) ↔ x Clos1 ({M}, {p, q (p NC q NC q = (2cc p))})z((x S x{p, q (p NC q NC q = (2cc p))}z) → z S)))
652, 64syl 15 . . . . . . 7 (M NC → (x ( SpacM)z((x S x{p, q (p NC q NC q = (2cc p))}z) → z S) ↔ x Clos1 ({M}, {p, q (p NC q NC q = (2cc p))})z((x S x{p, q (p NC q NC q = (2cc p))}z) → z S)))
6663, 65sylibd 205 . . . . . 6 (M NC → (x ( SpacM)((x S (xc 0c) NC ) → (2cc x) S) → x Clos1 ({M}, {p, q (p NC q NC q = (2cc p))})z((x S x{p, q (p NC q NC q = (2cc p))}z) → z S)))
6766imp 418 . . . . 5 ((M NC x ( SpacM)((x S (xc 0c) NC ) → (2cc x) S)) → x Clos1 ({M}, {p, q (p NC q NC q = (2cc p))})z((x S x{p, q (p NC q NC q = (2cc p))}z) → z S))
6867ad2ant2rl 729 . . . 4 (((M NC S V) (M S x ( SpacM)((x S (xc 0c) NC ) → (2cc x) S))) → x Clos1 ({M}, {p, q (p NC q NC q = (2cc p))})z((x S x{p, q (p NC q NC q = (2cc p))}z) → z S))
69 snex 4111 . . . . 5 {M} V
70 spacvallem1 6281 . . . . 5 {p, q (p NC q NC q = (2cc p))} V
71 eqid 2353 . . . . 5 Clos1 ({M}, {p, q (p NC q NC q = (2cc p))}) = Clos1 ({M}, {p, q (p NC q NC q = (2cc p))})
7269, 70, 71clos1induct 5880 . . . 4 ((S V {M} S x Clos1 ({M}, {p, q (p NC q NC q = (2cc p))})z((x S x{p, q (p NC q NC q = (2cc p))}z) → z S)) → Clos1 ({M}, {p, q (p NC q NC q = (2cc p))}) S)
735, 8, 68, 72syl3anc 1182 . . 3 (((M NC S V) (M S x ( SpacM)((x S (xc 0c) NC ) → (2cc x) S))) → Clos1 ({M}, {p, q (p NC q NC q = (2cc p))}) S)
744, 73eqsstrd 3305 . 2 (((M NC S V) (M S x ( SpacM)((x S (xc 0c) NC ) → (2cc x) S))) → ( SpacM) S)
751, 74sylanl2 632 1 (((M NC S V) (M S x ( SpacM)((x S (xc 0c) NC ) → (2cc x) S))) → ( SpacM) S)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176   wa 358   w3a 934  wal 1540   = wceq 1642   wcel 1710  wral 2614  Vcvv 2859   wss 3257  {csn 3737  0cc0c 4374  {copab 4622   class class class wbr 4639  cfv 4781  (class class class)co 5525   Clos1 cclos1 5872   NC cncs 6088  2cc2c 6094  c cce 6096   Spac cspac 6273
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-ov 5526  df-oprab 5528  df-mpt 5652  df-mpt2 5654  df-txp 5736  df-fix 5740  df-compose 5748  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-fullfun 5768  df-clos1 5873  df-trans 5899  df-sym 5908  df-er 5909  df-ec 5947  df-qs 5951  df-map 6001  df-en 6029  df-ncs 6098  df-nc 6101  df-2c 6104  df-ce 6106  df-spac 6274
This theorem is referenced by:  spacis  6288  nchoicelem6  6294
  Copyright terms: Public domain W3C validator