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

Theorem nchoicelem17 6305
Description: Lemma for nchoice 6308. If the special set of a cardinal is finite, then so is the special set of its T-raising, and there is a calculable relationship between their sizes. Theorem 7.2 of [Specker] p. 974. (Contributed by SF, 19-Mar-2015.)
Assertion
Ref Expression
nchoicelem17 (( ≤c We NC M NC ( SpacM) Fin ) → (( SpacTc M) Fin ( Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 1c) Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 2c))))

Proof of Theorem nchoicelem17
Dummy variables k m n t x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 finnc 6243 . . 3 (( SpacM) FinNc ( SpacM) Nn )
2 risset 2661 . . . 4 ( Nc ( SpacM) Nnt Nn t = Nc ( SpacM))
3 nchoicelem13 6301 . . . . . . 7 (M NC → 1cc Nc ( SpacM))
43ad2antlr 707 . . . . . 6 ((( ≤c We NC M NC ) t Nn ) → 1cc Nc ( SpacM))
5 1cnc 6139 . . . . . . . 8 1c NC
6 fvex 5339 . . . . . . . . 9 ( SpacM) V
76ncelncsi 6121 . . . . . . . 8 Nc ( SpacM) NC
8 dflec2 6210 . . . . . . . 8 ((1c NC Nc ( SpacM) NC ) → (1cc Nc ( SpacM) ↔ x NC Nc ( SpacM) = (1c +c x)))
95, 7, 8mp2an 653 . . . . . . 7 (1cc Nc ( SpacM) ↔ x NC Nc ( SpacM) = (1c +c x))
10 eqtr 2370 . . . . . . . . . . . 12 ((t = Nc ( SpacM) Nc ( SpacM) = (1c +c x)) → t = (1c +c x))
1110ancoms 439 . . . . . . . . . . 11 (( Nc ( SpacM) = (1c +c x) t = Nc ( SpacM)) → t = (1c +c x))
12 eqtr2 2371 . . . . . . . . . . . . 13 ((t = Nc ( SpacM) t = (1c +c x)) → Nc ( SpacM) = (1c +c x))
1312ex 423 . . . . . . . . . . . 12 (t = Nc ( SpacM) → (t = (1c +c x) → Nc ( SpacM) = (1c +c x)))
1413adantl 452 . . . . . . . . . . 11 (( Nc ( SpacM) = (1c +c x) t = Nc ( SpacM)) → (t = (1c +c x) → Nc ( SpacM) = (1c +c x)))
1511, 14jcai 522 . . . . . . . . . 10 (( Nc ( SpacM) = (1c +c x) t = Nc ( SpacM)) → (t = (1c +c x) Nc ( SpacM) = (1c +c x)))
16 addceq2 4384 . . . . . . . . . . . . . . . . . 18 (k = 1c → (x +c k) = (x +c 1c))
17 addccom 4406 . . . . . . . . . . . . . . . . . 18 (x +c 1c) = (1c +c x)
1816, 17syl6eq 2401 . . . . . . . . . . . . . . . . 17 (k = 1c → (x +c k) = (1c +c x))
1918eqeq2d 2364 . . . . . . . . . . . . . . . 16 (k = 1c → (t = (x +c k) ↔ t = (1c +c x)))
2019rspcev 2955 . . . . . . . . . . . . . . 15 ((1c NC t = (1c +c x)) → k NC t = (x +c k))
215, 20mpan 651 . . . . . . . . . . . . . 14 (t = (1c +c x) → k NC t = (x +c k))
22 nnnc 6146 . . . . . . . . . . . . . . . 16 (t Nnt NC )
23 dflec2 6210 . . . . . . . . . . . . . . . 16 ((x NC t NC ) → (xc tk NC t = (x +c k)))
2422, 23sylan2 460 . . . . . . . . . . . . . . 15 ((x NC t Nn ) → (xc tk NC t = (x +c k)))
2524ancoms 439 . . . . . . . . . . . . . 14 ((t Nn x NC ) → (xc tk NC t = (x +c k)))
2621, 25syl5ibr 212 . . . . . . . . . . . . 13 ((t Nn x NC ) → (t = (1c +c x) → xc t))
2726adantll 694 . . . . . . . . . . . 12 (((( ≤c We NC M NC ) t Nn ) x NC ) → (t = (1c +c x) → xc t))
28 nclenn 6249 . . . . . . . . . . . . . . 15 ((x NC t Nn xc t) → x Nn )
29283expia 1153 . . . . . . . . . . . . . 14 ((x NC t Nn ) → (xc tx Nn ))
3029ancoms 439 . . . . . . . . . . . . 13 ((t Nn x NC ) → (xc tx Nn ))
3130adantll 694 . . . . . . . . . . . 12 (((( ≤c We NC M NC ) t Nn ) x NC ) → (xc tx Nn ))
32 nchoicelem16 6304 . . . . . . . . . . . . . . . . . 18 {t ( ≤c We NCm NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))))} V
33 addceq2 4384 . . . . . . . . . . . . . . . . . . . . . . 23 (t = 0c → (1c +c t) = (1c +c 0c))
34 addcid1 4405 . . . . . . . . . . . . . . . . . . . . . . 23 (1c +c 0c) = 1c
3533, 34syl6eq 2401 . . . . . . . . . . . . . . . . . . . . . 22 (t = 0c → (1c +c t) = 1c)
3635eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . 21 (t = 0c → ( Nc ( Spacm) = (1c +c t) ↔ Nc ( Spacm) = 1c))
3736imbi1d 308 . . . . . . . . . . . . . . . . . . . 20 (t = 0c → (( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) ↔ ( Nc ( Spacm) = 1c → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))))
3837ralbidv 2634 . . . . . . . . . . . . . . . . . . 19 (t = 0c → (m NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) ↔ m NC ( Nc ( Spacm) = 1c → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))))
3938imbi2d 307 . . . . . . . . . . . . . . . . . 18 (t = 0c → (( ≤c We NCm NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))) ↔ ( ≤c We NCm NC ( Nc ( Spacm) = 1c → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))))))
40 addceq2 4384 . . . . . . . . . . . . . . . . . . . . . 22 (t = n → (1c +c t) = (1c +c n))
4140eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . 21 (t = n → ( Nc ( Spacm) = (1c +c t) ↔ Nc ( Spacm) = (1c +c n)))
4241imbi1d 308 . . . . . . . . . . . . . . . . . . . 20 (t = n → (( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) ↔ ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))))
4342ralbidv 2634 . . . . . . . . . . . . . . . . . . 19 (t = n → (m NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) ↔ m NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))))
4443imbi2d 307 . . . . . . . . . . . . . . . . . 18 (t = n → (( ≤c We NCm NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))) ↔ ( ≤c We NCm NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))))))
45 addceq2 4384 . . . . . . . . . . . . . . . . . . . . . . 23 (t = (n +c 1c) → (1c +c t) = (1c +c (n +c 1c)))
4645eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . . 22 (t = (n +c 1c) → ( Nc ( Spacm) = (1c +c t) ↔ Nc ( Spacm) = (1c +c (n +c 1c))))
4746imbi1d 308 . . . . . . . . . . . . . . . . . . . . 21 (t = (n +c 1c) → (( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) ↔ ( Nc ( Spacm) = (1c +c (n +c 1c)) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))))
4847ralbidv 2634 . . . . . . . . . . . . . . . . . . . 20 (t = (n +c 1c) → (m NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) ↔ m NC ( Nc ( Spacm) = (1c +c (n +c 1c)) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))))
49 fveq2 5328 . . . . . . . . . . . . . . . . . . . . . . . 24 (m = k → ( Spacm) = ( Spack))
5049nceqd 6110 . . . . . . . . . . . . . . . . . . . . . . 23 (m = kNc ( Spacm) = Nc ( Spack))
5150eqeq1d 2361 . . . . . . . . . . . . . . . . . . . . . 22 (m = k → ( Nc ( Spacm) = (1c +c (n +c 1c)) ↔ Nc ( Spack) = (1c +c (n +c 1c))))
52 tceq 6158 . . . . . . . . . . . . . . . . . . . . . . . . 25 (m = kTc m = Tc k)
5352fveq2d 5332 . . . . . . . . . . . . . . . . . . . . . . . 24 (m = k → ( SpacTc m) = ( SpacTc k))
5453eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . 23 (m = k → (( SpacTc m) Fin ↔ ( SpacTc k) Fin ))
5553nceqd 6110 . . . . . . . . . . . . . . . . . . . . . . . . 25 (m = kNc ( SpacTc m) = Nc ( SpacTc k))
56 tceq 6158 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ( Nc ( Spacm) = Nc ( Spack) → Tc Nc ( Spacm) = Tc Nc ( Spack))
5750, 56syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (m = kTc Nc ( Spacm) = Tc Nc ( Spack))
5857addceq1d 4389 . . . . . . . . . . . . . . . . . . . . . . . . 25 (m = k → ( Tc Nc ( Spacm) +c 1c) = ( Tc Nc ( Spack) +c 1c))
5955, 58eqeq12d 2367 . . . . . . . . . . . . . . . . . . . . . . . 24 (m = k → ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) ↔ Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c)))
6057addceq1d 4389 . . . . . . . . . . . . . . . . . . . . . . . . 25 (m = k → ( Tc Nc ( Spacm) +c 2c) = ( Tc Nc ( Spack) +c 2c))
6155, 60eqeq12d 2367 . . . . . . . . . . . . . . . . . . . . . . . 24 (m = k → ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c) ↔ Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c)))
6259, 61orbi12d 690 . . . . . . . . . . . . . . . . . . . . . . 23 (m = k → (( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)) ↔ ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c))))
6354, 62anbi12d 691 . . . . . . . . . . . . . . . . . . . . . 22 (m = k → ((( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))) ↔ (( SpacTc k) Fin ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c)))))
6451, 63imbi12d 311 . . . . . . . . . . . . . . . . . . . . 21 (m = k → (( Nc ( Spacm) = (1c +c (n +c 1c)) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) ↔ ( Nc ( Spack) = (1c +c (n +c 1c)) → (( SpacTc k) Fin ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c))))))
6564cbvralv 2835 . . . . . . . . . . . . . . . . . . . 20 (m NC ( Nc ( Spacm) = (1c +c (n +c 1c)) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) ↔ k NC ( Nc ( Spack) = (1c +c (n +c 1c)) → (( SpacTc k) Fin ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c)))))
6648, 65syl6bb 252 . . . . . . . . . . . . . . . . . . 19 (t = (n +c 1c) → (m NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) ↔ k NC ( Nc ( Spack) = (1c +c (n +c 1c)) → (( SpacTc k) Fin ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c))))))
6766imbi2d 307 . . . . . . . . . . . . . . . . . 18 (t = (n +c 1c) → (( ≤c We NCm NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))) ↔ ( ≤c We NCk NC ( Nc ( Spack) = (1c +c (n +c 1c)) → (( SpacTc k) Fin ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c)))))))
68 addceq2 4384 . . . . . . . . . . . . . . . . . . . . . 22 (t = x → (1c +c t) = (1c +c x))
6968eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . 21 (t = x → ( Nc ( Spacm) = (1c +c t) ↔ Nc ( Spacm) = (1c +c x)))
7069imbi1d 308 . . . . . . . . . . . . . . . . . . . 20 (t = x → (( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) ↔ ( Nc ( Spacm) = (1c +c x) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))))
7170ralbidv 2634 . . . . . . . . . . . . . . . . . . 19 (t = x → (m NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) ↔ m NC ( Nc ( Spacm) = (1c +c x) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))))
7271imbi2d 307 . . . . . . . . . . . . . . . . . 18 (t = x → (( ≤c We NCm NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))) ↔ ( ≤c We NCm NC ( Nc ( Spacm) = (1c +c x) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))))))
73 nchoicelem14 6302 . . . . . . . . . . . . . . . . . . . . . 22 ((m NC Nc ( Spacm) = 1c) → ¬ (mc 0c) NC )
7473ex 423 . . . . . . . . . . . . . . . . . . . . 21 (m NC → ( Nc ( Spacm) = 1c → ¬ (mc 0c) NC ))
7574adantl 452 . . . . . . . . . . . . . . . . . . . 20 (( ≤c We NC m NC ) → ( Nc ( Spacm) = 1c → ¬ (mc 0c) NC ))
76 nchoicelem9 6297 . . . . . . . . . . . . . . . . . . . . . . 23 (( ≤c We NC m NC ¬ (mc 0c) NC ) → ( Nc ( SpacTc m) = 2c Nc ( SpacTc m) = 3c))
77 id 19 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ( Nc ( SpacTc m) = 2cNc ( SpacTc m) = 2c)
78 2nnc 6167 . . . . . . . . . . . . . . . . . . . . . . . . . 26 2c Nn
7977, 78syl6eqel 2441 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( Nc ( SpacTc m) = 2cNc ( SpacTc m) Nn )
80 id 19 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ( Nc ( SpacTc m) = 3cNc ( SpacTc m) = 3c)
81 2p1e3c 6156 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (2c +c 1c) = 3c
82 peano2 4403 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (2c Nn → (2c +c 1c) Nn )
8378, 82ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (2c +c 1c) Nn
8481, 83eqeltrri 2424 . . . . . . . . . . . . . . . . . . . . . . . . . 26 3c Nn
8580, 84syl6eqel 2441 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( Nc ( SpacTc m) = 3cNc ( SpacTc m) Nn )
8679, 85jaoi 368 . . . . . . . . . . . . . . . . . . . . . . . 24 (( Nc ( SpacTc m) = 2c Nc ( SpacTc m) = 3c) → Nc ( SpacTc m) Nn )
87 finnc 6243 . . . . . . . . . . . . . . . . . . . . . . . 24 (( SpacTc m) FinNc ( SpacTc m) Nn )
8886, 87sylibr 203 . . . . . . . . . . . . . . . . . . . . . . 23 (( Nc ( SpacTc m) = 2c Nc ( SpacTc m) = 3c) → ( SpacTc m) Fin )
8976, 88syl 15 . . . . . . . . . . . . . . . . . . . . . 22 (( ≤c We NC m NC ¬ (mc 0c) NC ) → ( SpacTc m) Fin )
90 1p1e2c 6155 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1c +c 1c) = 2c
9190eqeq2i 2363 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( Nc ( SpacTc m) = (1c +c 1c) ↔ Nc ( SpacTc m) = 2c)
92 addccom 4406 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (1c +c 2c) = (2c +c 1c)
9392, 81eqtri 2373 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1c +c 2c) = 3c
9493eqeq2i 2363 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( Nc ( SpacTc m) = (1c +c 2c) ↔ Nc ( SpacTc m) = 3c)
9591, 94orbi12i 507 . . . . . . . . . . . . . . . . . . . . . . . 24 (( Nc ( SpacTc m) = (1c +c 1c) Nc ( SpacTc m) = (1c +c 2c)) ↔ ( Nc ( SpacTc m) = 2c Nc ( SpacTc m) = 3c))
9676, 95sylibr 203 . . . . . . . . . . . . . . . . . . . . . . 23 (( ≤c We NC m NC ¬ (mc 0c) NC ) → ( Nc ( SpacTc m) = (1c +c 1c) Nc ( SpacTc m) = (1c +c 2c)))
97 nchoicelem3 6291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((m NC ¬ (mc 0c) NC ) → ( Spacm) = {m})
9897nceqd 6110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((m NC ¬ (mc 0c) NC ) → Nc ( Spacm) = Nc {m})
99 df1c3g 6141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (m NC → 1c = Nc {m})
10099adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((m NC ¬ (mc 0c) NC ) → 1c = Nc {m})
10198, 100eqtr4d 2388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((m NC ¬ (mc 0c) NC ) → Nc ( Spacm) = 1c)
102 tceq 6158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ( Nc ( Spacm) = 1cTc Nc ( Spacm) = Tc 1c)
103101, 102syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((m NC ¬ (mc 0c) NC ) → Tc Nc ( Spacm) = Tc 1c)
104 tc1c 6165 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Tc 1c = 1c
105103, 104syl6eq 2401 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((m NC ¬ (mc 0c) NC ) → Tc Nc ( Spacm) = 1c)
106105addceq1d 4389 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((m NC ¬ (mc 0c) NC ) → ( Tc Nc ( Spacm) +c 1c) = (1c +c 1c))
107106eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((m NC ¬ (mc 0c) NC ) → ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) ↔ Nc ( SpacTc m) = (1c +c 1c)))
108105addceq1d 4389 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((m NC ¬ (mc 0c) NC ) → ( Tc Nc ( Spacm) +c 2c) = (1c +c 2c))
109108eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((m NC ¬ (mc 0c) NC ) → ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c) ↔ Nc ( SpacTc m) = (1c +c 2c)))
110107, 109orbi12d 690 . . . . . . . . . . . . . . . . . . . . . . . 24 ((m NC ¬ (mc 0c) NC ) → (( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)) ↔ ( Nc ( SpacTc m) = (1c +c 1c) Nc ( SpacTc m) = (1c +c 2c))))
1111103adant1 973 . . . . . . . . . . . . . . . . . . . . . . 23 (( ≤c We NC m NC ¬ (mc 0c) NC ) → (( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)) ↔ ( Nc ( SpacTc m) = (1c +c 1c) Nc ( SpacTc m) = (1c +c 2c))))
11296, 111mpbird 223 . . . . . . . . . . . . . . . . . . . . . 22 (( ≤c We NC m NC ¬ (mc 0c) NC ) → ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))
11389, 112jca 518 . . . . . . . . . . . . . . . . . . . . 21 (( ≤c We NC m NC ¬ (mc 0c) NC ) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))
1141133expia 1153 . . . . . . . . . . . . . . . . . . . 20 (( ≤c We NC m NC ) → (¬ (mc 0c) NC → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))))
11575, 114syld 40 . . . . . . . . . . . . . . . . . . 19 (( ≤c We NC m NC ) → ( Nc ( Spacm) = 1c → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))))
116115ralrimiva 2697 . . . . . . . . . . . . . . . . . 18 ( ≤c We NCm NC ( Nc ( Spacm) = 1c → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))))
117 addccom 4406 . . . . . . . . . . . . . . . . . . . . . . . 24 (1c +c (n +c 1c)) = ((n +c 1c) +c 1c)
118117eqeq2i 2363 . . . . . . . . . . . . . . . . . . . . . . 23 ( Nc ( Spack) = (1c +c (n +c 1c)) ↔ Nc ( Spack) = ((n +c 1c) +c 1c))
119 nchoicelem13 6301 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (k NC → 1cc Nc ( Spack))
120119ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((( ≤c We NC n Nn m NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))) (k NC Nc ( Spack) = ((n +c 1c) +c 1c))) → 1cc Nc ( Spack))
121 simp2 956 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (( ≤c We NC n Nn m NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))) → n Nn )
122 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((k NC Nc ( Spack) = ((n +c 1c) +c 1c)) → Nc ( Spack) = ((n +c 1c) +c 1c))
123 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((n Nn Nc ( Spack) = ((n +c 1c) +c 1c)) → Nc ( Spack) = ((n +c 1c) +c 1c))
124 0cnsuc 4401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (n +c 1c) ≠ 0c
125 peano2 4403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (n Nn → (n +c 1c) Nn )
126 peano1 4402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 0c Nn
127 1cnnc 4408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 1c Nn
128 addccan1 4560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((n +c 1c) Nn 0c Nn 1c Nn ) → (((n +c 1c) +c 1c) = (0c +c 1c) ↔ (n +c 1c) = 0c))
129126, 127, 128mp3an23 1269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((n +c 1c) Nn → (((n +c 1c) +c 1c) = (0c +c 1c) ↔ (n +c 1c) = 0c))
130125, 129syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (n Nn → (((n +c 1c) +c 1c) = (0c +c 1c) ↔ (n +c 1c) = 0c))
131130necon3bid 2551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (n Nn → (((n +c 1c) +c 1c) ≠ (0c +c 1c) ↔ (n +c 1c) ≠ 0c))
132124, 131mpbiri 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (n Nn → ((n +c 1c) +c 1c) ≠ (0c +c 1c))
133 addcid2 4407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (0c +c 1c) = 1c
134133neeq2i 2527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((n +c 1c) +c 1c) ≠ (0c +c 1c) ↔ ((n +c 1c) +c 1c) ≠ 1c)
135132, 134sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (n Nn → ((n +c 1c) +c 1c) ≠ 1c)
136135adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((n Nn Nc ( Spack) = ((n +c 1c) +c 1c)) → ((n +c 1c) +c 1c) ≠ 1c)
137123, 136eqnetrd 2534 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((n Nn Nc ( Spack) = ((n +c 1c) +c 1c)) → Nc ( Spack) ≠ 1c)
138121, 122, 137syl2an 463 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((( ≤c We NC n Nn m NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))) (k NC Nc ( Spack) = ((n +c 1c) +c 1c))) → Nc ( Spack) ≠ 1c)
139138necomd 2599 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((( ≤c We NC n Nn m NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))) (k NC Nc ( Spack) = ((n +c 1c) +c 1c))) → 1cNc ( Spack))
140 brltc 6114 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1c <c Nc ( Spack) ↔ (1cc Nc ( Spack) 1cNc ( Spack)))
141120, 139, 140sylanbrc 645 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( ≤c We NC n Nn m NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))) (k NC Nc ( Spack) = ((n +c 1c) +c 1c))) → 1c <c Nc ( Spack))
142 nchoicelem15 6303 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((k NC 1c <c Nc ( Spack)) → (kc 0c) NC )
143142ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (k NC → (1c <c Nc ( Spack) → (kc 0c) NC ))
144143ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((( ≤c We NC n Nn m NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))) (k NC Nc ( Spack) = ((n +c 1c) +c 1c))) → (1c <c Nc ( Spack) → (kc 0c) NC ))
145 df-3an 936 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC ) ↔ ((k NC Nc ( Spack) = ((n +c 1c) +c 1c)) (kc 0c) NC ))
146 ceclnn1 6189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((2c Nn k NC (kc 0c) NC ) → (2cc k) NC )
14778, 146mp3an1 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((k NC (kc 0c) NC ) → (2cc k) NC )
1481473adant2 974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC ) → (2cc k) NC )
149148adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((( ≤c We NC n Nn m NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → (2cc k) NC )
150 fveq2 5328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (m = (2cc k) → ( Spacm) = ( Spac ‘(2cc k)))
151150nceqd 6110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (m = (2cc k) → Nc ( Spacm) = Nc ( Spac ‘(2cc k)))
152151eqeq1d 2361 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (m = (2cc k) → ( Nc ( Spacm) = (1c +c n) ↔ Nc ( Spac ‘(2cc k)) = (1c +c n)))
153 tceq 6158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (m = (2cc k) → Tc m = Tc (2cc k))
154153fveq2d 5332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (m = (2cc k) → ( SpacTc m) = ( SpacTc (2cc k)))
155154eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (m = (2cc k) → (( SpacTc m) Fin ↔ ( SpacTc (2cc k)) Fin ))
156154nceqd 6110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (m = (2cc k) → Nc ( SpacTc m) = Nc ( SpacTc (2cc k)))
157 tceq 6158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ( Nc ( Spacm) = Nc ( Spac ‘(2cc k)) → Tc Nc ( Spacm) = Tc Nc ( Spac ‘(2cc k)))
158151, 157syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (m = (2cc k) → Tc Nc ( Spacm) = Tc Nc ( Spac ‘(2cc k)))
159158addceq1d 4389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (m = (2cc k) → ( Tc Nc ( Spacm) +c 1c) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c))
160156, 159eqeq12d 2367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (m = (2cc k) → ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) ↔ Nc ( SpacTc (2cc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c)))
161158addceq1d 4389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (m = (2cc k) → ( Tc Nc ( Spacm) +c 2c) = ( Tc Nc ( Spac ‘(2cc k)) +c 2c))
162156, 161eqeq12d 2367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (m = (2cc k) → ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c) ↔ Nc ( SpacTc (2cc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 2c)))
163160, 162orbi12d 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (m = (2cc k) → (( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)) ↔ ( Nc ( SpacTc (2cc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c) Nc ( SpacTc (2cc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 2c))))
164155, 163anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (m = (2cc k) → ((( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))) ↔ (( SpacTc (2cc k)) Fin ( Nc ( SpacTc (2cc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c) Nc ( SpacTc (2cc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 2c)))))
165152, 164imbi12d 311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (m = (2cc k) → (( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) ↔ ( Nc ( Spac ‘(2cc k)) = (1c +c n) → (( SpacTc (2cc k)) Fin ( Nc ( SpacTc (2cc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c) Nc ( SpacTc (2cc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 2c))))))
166165rspccva 2954 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((m NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) (2cc k) NC ) → ( Nc ( Spac ‘(2cc k)) = (1c +c n) → (( SpacTc (2cc k)) Fin ( Nc ( SpacTc (2cc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c) Nc ( SpacTc (2cc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 2c)))))
167 tce2 6236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((k NC (kc 0c) NC ) → Tc (2cc k) = (2cc Tc k))
168167fveq2d 5332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((k NC (kc 0c) NC ) → ( SpacTc (2cc k)) = ( Spac ‘(2cc Tc k)))
169168eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((k NC (kc 0c) NC ) → (( SpacTc (2cc k)) Fin ↔ ( Spac ‘(2cc Tc k)) Fin ))
170168nceqd 6110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((k NC (kc 0c) NC ) → Nc ( SpacTc (2cc k)) = Nc ( Spac ‘(2cc Tc k)))
171170eqeq1d 2361 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((k NC (kc 0c) NC ) → ( Nc ( SpacTc (2cc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c) ↔ Nc ( Spac ‘(2cc Tc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c)))
172170eqeq1d 2361 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((k NC (kc 0c) NC ) → ( Nc ( SpacTc (2cc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 2c) ↔ Nc ( Spac ‘(2cc Tc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 2c)))
173171, 172orbi12d 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((k NC (kc 0c) NC ) → (( Nc ( SpacTc (2cc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c) Nc ( SpacTc (2cc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 2c)) ↔ ( Nc ( Spac ‘(2cc Tc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c) Nc ( Spac ‘(2cc Tc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 2c))))
174169, 173anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((k NC (kc 0c) NC ) → ((( SpacTc (2cc k)) Fin ( Nc ( SpacTc (2cc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c) Nc ( SpacTc (2cc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 2c))) ↔ (( Spac ‘(2cc Tc k)) Fin ( Nc ( Spac ‘(2cc Tc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c) Nc ( Spac ‘(2cc Tc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 2c)))))
175174imbi2d 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((k NC (kc 0c) NC ) → (( Nc ( Spac ‘(2cc k)) = (1c +c n) → (( SpacTc (2cc k)) Fin ( Nc ( SpacTc (2cc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c) Nc ( SpacTc (2cc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 2c)))) ↔ ( Nc ( Spac ‘(2cc k)) = (1c +c n) → (( Spac ‘(2cc Tc k)) Fin ( Nc ( Spac ‘(2cc Tc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c) Nc ( Spac ‘(2cc Tc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 2c))))))
1761753adant2 974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC ) → (( Nc ( Spac ‘(2cc k)) = (1c +c n) → (( SpacTc (2cc k)) Fin ( Nc ( SpacTc (2cc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c) Nc ( SpacTc (2cc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 2c)))) ↔ ( Nc ( Spac ‘(2cc k)) = (1c +c n) → (( Spac ‘(2cc Tc k)) Fin ( Nc ( Spac ‘(2cc Tc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c) Nc ( Spac ‘(2cc Tc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 2c))))))
177176adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((( ≤c We NC n Nn ) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → (( Nc ( Spac ‘(2cc k)) = (1c +c n) → (( SpacTc (2cc k)) Fin ( Nc ( SpacTc (2cc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c) Nc ( SpacTc (2cc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 2c)))) ↔ ( Nc ( Spac ‘(2cc k)) = (1c +c n) → (( Spac ‘(2cc Tc k)) Fin ( Nc ( Spac ‘(2cc Tc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c) Nc ( Spac ‘(2cc Tc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 2c))))))
178 nchoicelem7 6295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((k NC (kc 0c) NC ) → Nc ( Spack) = ( Nc ( Spac ‘(2cc k)) +c 1c))
1791783adant2 974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC ) → Nc ( Spack) = ( Nc ( Spac ‘(2cc k)) +c 1c))
180 simp2 956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC ) → Nc ( Spack) = ((n +c 1c) +c 1c))
181179, 180eqtr3d 2387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC ) → ( Nc ( Spac ‘(2cc k)) +c 1c) = ((n +c 1c) +c 1c))
182181adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((( ≤c We NC n Nn ) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → ( Nc ( Spac ‘(2cc k)) +c 1c) = ((n +c 1c) +c 1c))
183 nnnc 6146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((n +c 1c) Nn → (n +c 1c) NC )
184 fvex 5339 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ( Spac ‘(2cc k)) V
185184ncelncsi 6121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 Nc ( Spac ‘(2cc k)) NC
186 peano4nc 6150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (( Nc ( Spac ‘(2cc k)) NC (n +c 1c) NC ) → (( Nc ( Spac ‘(2cc k)) +c 1c) = ((n +c 1c) +c 1c) ↔ Nc ( Spac ‘(2cc k)) = (n +c 1c)))
187185, 186mpan 651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((n +c 1c) NC → (( Nc ( Spac ‘(2cc k)) +c 1c) = ((n +c 1c) +c 1c) ↔ Nc ( Spac ‘(2cc k)) = (n +c 1c)))
188125, 183, 1873syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (n Nn → (( Nc ( Spac ‘(2cc k)) +c 1c) = ((n +c 1c) +c 1c) ↔ Nc ( Spac ‘(2cc k)) = (n +c 1c)))
189188ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((( ≤c We NC n Nn ) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → (( Nc ( Spac ‘(2cc k)) +c 1c) = ((n +c 1c) +c 1c) ↔ Nc ( Spac ‘(2cc k)) = (n +c 1c)))
190182, 189mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((( ≤c We NC n Nn ) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → Nc ( Spac ‘(2cc k)) = (n +c 1c))
191 addccom 4406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (n +c 1c) = (1c +c n)
192190, 191syl6eq 2401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((( ≤c We NC n Nn ) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → Nc ( Spac ‘(2cc k)) = (1c +c n))
193 peano2 4403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ( Nc ( Spac ‘(2cc Tc k)) Nn → ( Nc ( Spac ‘(2cc Tc k)) +c 1c) Nn )
194 tccl 6160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (k NCTc k NC )
195 te0c 6237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (k NC → ( Tc kc 0c) NC )
196 nchoicelem7 6295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (( Tc k NC ( Tc kc 0c) NC ) → Nc ( SpacTc k) = ( Nc ( Spac ‘(2cc Tc k)) +c 1c))
197194, 195, 196syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (k NCNc ( SpacTc k) = ( Nc ( Spac ‘(2cc Tc k)) +c 1c))
1981973ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC ) → Nc ( SpacTc k) = ( Nc ( Spac ‘(2cc Tc k)) +c 1c))
199198adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((( ≤c We NC n Nn ) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → Nc ( SpacTc k) = ( Nc ( Spac ‘(2cc Tc k)) +c 1c))
200199eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((( ≤c We NC n Nn ) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → ( Nc ( SpacTc k) Nn ↔ ( Nc ( Spac ‘(2cc Tc k)) +c 1c) Nn ))
201193, 200syl5ibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((( ≤c We NC n Nn ) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → ( Nc ( Spac ‘(2cc Tc k)) NnNc ( SpacTc k) Nn ))
202 finnc 6243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (( Spac ‘(2cc Tc k)) FinNc ( Spac ‘(2cc Tc k)) Nn )
203 finnc 6243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (( SpacTc k) FinNc ( SpacTc k) Nn )
204201, 202, 2033imtr4g 261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((( ≤c We NC n Nn ) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → (( Spac ‘(2cc Tc k)) Fin → ( SpacTc k) Fin ))
205 addceq1 4383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ( Nc ( Spac ‘(2cc Tc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c) → ( Nc ( Spac ‘(2cc Tc k)) +c 1c) = (( Tc Nc ( Spac ‘(2cc k)) +c 1c) +c 1c))
206 tceq 6158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ( Nc ( Spack) = ( Nc ( Spac ‘(2cc k)) +c 1c) → Tc Nc ( Spack) = Tc ( Nc ( Spac ‘(2cc k)) +c 1c))
207178, 206syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((k NC (kc 0c) NC ) → Tc Nc ( Spack) = Tc ( Nc ( Spac ‘(2cc k)) +c 1c))
2082073adant2 974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC ) → Tc Nc ( Spack) = Tc ( Nc ( Spac ‘(2cc k)) +c 1c))
209208adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((( ≤c We NC n Nn ) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → Tc Nc ( Spack) = Tc ( Nc ( Spac ‘(2cc k)) +c 1c))
210 tcdi 6164 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (( Nc ( Spac ‘(2cc k)) NC 1c NC ) → Tc ( Nc ( Spac ‘(2cc k)) +c 1c) = ( Tc Nc ( Spac ‘(2cc k)) +c Tc 1c))
211185, 5, 210mp2an 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Tc ( Nc ( Spac ‘(2cc k)) +c 1c) = ( Tc Nc ( Spac ‘(2cc k)) +c Tc 1c)
212104addceq2i 4387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ( Tc Nc ( Spac ‘(2cc k)) +c Tc 1c) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c)
213211, 212eqtri 2373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Tc ( Nc ( Spac ‘(2cc k)) +c 1c) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c)
214209, 213syl6eq 2401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((( ≤c We NC n Nn ) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → Tc Nc ( Spack) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c))
215214addceq1d 4389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((( ≤c We NC n Nn ) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → ( Tc Nc ( Spack) +c 1c) = (( Tc Nc ( Spac ‘(2cc k)) +c 1c) +c 1c))
216199, 215eqeq12d 2367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((( ≤c We NC n Nn ) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) ↔ ( Nc ( Spac ‘(2cc Tc k)) +c 1c) = (( Tc Nc ( Spac ‘(2cc k)) +c 1c) +c 1c)))
217205, 216syl5ibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((( ≤c We NC n Nn ) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → ( Nc ( Spac ‘(2cc Tc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c) → Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c)))
218 addceq1 4383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ( Nc ( Spac ‘(2cc Tc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 2c) → ( Nc ( Spac ‘(2cc Tc k)) +c 1c) = (( Tc Nc ( Spac ‘(2cc k)) +c 2c) +c 1c))
219214addceq1d 4389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((( ≤c We NC n Nn ) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → ( Tc Nc ( Spack) +c 2c) = (( Tc Nc ( Spac ‘(2cc k)) +c 1c) +c 2c))
220 addc32 4416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (( Tc Nc ( Spac ‘(2cc k)) +c 1c) +c 2c) = (( Tc Nc ( Spac ‘(2cc k)) +c 2c) +c 1c)
221219, 220syl6eq 2401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((( ≤c We NC n Nn ) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → ( Tc Nc ( Spack) +c 2c) = (( Tc Nc ( Spac ‘(2cc k)) +c 2c) +c 1c))
222199, 221eqeq12d 2367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((( ≤c We NC n Nn ) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c) ↔ ( Nc ( Spac ‘(2cc Tc k)) +c 1c) = (( Tc Nc ( Spac ‘(2cc k)) +c 2c) +c 1c)))
223218, 222syl5ibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((( ≤c We NC n Nn ) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → ( Nc ( Spac ‘(2cc Tc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 2c) → Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c)))
224217, 223orim12d 811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((( ≤c We NC n Nn ) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → (( Nc ( Spac ‘(2cc Tc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c) Nc ( Spac ‘(2cc Tc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 2c)) → ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c))))
225204, 224anim12d 546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((( ≤c We NC n Nn ) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → ((( Spac ‘(2cc Tc k)) Fin ( Nc ( Spac ‘(2cc Tc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c) Nc ( Spac ‘(2cc Tc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 2c))) → (( SpacTc k) Fin ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c)))))
226192, 225embantd 50 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((( ≤c We NC n Nn ) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → (( Nc ( Spac ‘(2cc k)) = (1c +c n) → (( Spac ‘(2cc Tc k)) Fin ( Nc ( Spac ‘(2cc Tc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c) Nc ( Spac ‘(2cc Tc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 2c)))) → (( SpacTc k) Fin ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c)))))
227177, 226sylbid 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((( ≤c We NC n Nn ) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → (( Nc ( Spac ‘(2cc k)) = (1c +c n) → (( SpacTc (2cc k)) Fin ( Nc ( SpacTc (2cc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 1c) Nc ( SpacTc (2cc k)) = ( Tc Nc ( Spac ‘(2cc k)) +c 2c)))) → (( SpacTc k) Fin ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c)))))
228166, 227syl5 28 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((( ≤c We NC n Nn ) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → ((m NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) (2cc k) NC ) → (( SpacTc k) Fin ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c)))))
229228exp4b 590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ≤c We NC n Nn ) → ((k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC ) → (m NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) → ((2cc k) NC → (( SpacTc k) Fin ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c)))))))
230229com23 72 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (( ≤c We NC n Nn ) → (m NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) → ((k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC ) → ((2cc k) NC → (( SpacTc k) Fin ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c)))))))
2312303impia 1148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (( ≤c We NC n Nn m NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))) → ((k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC ) → ((2cc k) NC → (( SpacTc k) Fin ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c))))))
232231imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((( ≤c We NC n Nn m NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → ((2cc k) NC → (( SpacTc k) Fin ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c)))))
233149, 232mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((( ≤c We NC n Nn m NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))) (k NC Nc ( Spack) = ((n +c 1c) +c 1c) (kc 0c) NC )) → (( SpacTc k) Fin ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c))))
234145, 233sylan2br 462 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((( ≤c We NC n Nn m NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))) ((k NC Nc ( Spack) = ((n +c 1c) +c 1c)) (kc 0c) NC )) → (( SpacTc k) Fin ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c))))
235234expr 598 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((( ≤c We NC n Nn m NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))) (k NC Nc ( Spack) = ((n +c 1c) +c 1c))) → ((kc 0c) NC → (( SpacTc k) Fin ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c)))))
236144, 235syld 40 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( ≤c We NC n Nn m NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))) (k NC Nc ( Spack) = ((n +c 1c) +c 1c))) → (1c <c Nc ( Spack) → (( SpacTc k) Fin ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c)))))
237141, 236mpd 14 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( ≤c We NC n Nn m NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))) (k NC Nc ( Spack) = ((n +c 1c) +c 1c))) → (( SpacTc k) Fin ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c))))
238237expr 598 . . . . . . . . . . . . . . . . . . . . . . 23 ((( ≤c We NC n Nn m NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))) k NC ) → ( Nc ( Spack) = ((n +c 1c) +c 1c) → (( SpacTc k) Fin ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c)))))
239118, 238syl5bi 208 . . . . . . . . . . . . . . . . . . . . . 22 ((( ≤c We NC n Nn m NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))) k NC ) → ( Nc ( Spack) = (1c +c (n +c 1c)) → (( SpacTc k) Fin ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c)))))
240239ralrimiva 2697 . . . . . . . . . . . . . . . . . . . . 21 (( ≤c We NC n Nn m NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))) → k NC ( Nc ( Spack) = (1c +c (n +c 1c)) → (( SpacTc k) Fin ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c)))))
2412403exp 1150 . . . . . . . . . . . . . . . . . . . 20 ( ≤c We NC → (n Nn → (m NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) → k NC ( Nc ( Spack) = (1c +c (n +c 1c)) → (( SpacTc k) Fin ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c)))))))
242241com12 27 . . . . . . . . . . . . . . . . . . 19 (n Nn → ( ≤c We NC → (m NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) → k NC ( Nc ( Spack) = (1c +c (n +c 1c)) → (( SpacTc k) Fin ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c)))))))
243242a2d 23 . . . . . . . . . . . . . . . . . 18 (n Nn → (( ≤c We NCm NC ( Nc ( Spacm) = (1c +c n) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))) → ( ≤c We NCk NC ( Nc ( Spack) = (1c +c (n +c 1c)) → (( SpacTc k) Fin ( Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 1c) Nc ( SpacTc k) = ( Tc Nc ( Spack) +c 2c)))))))
24432, 39, 44, 67, 72, 116, 243finds 4411 . . . . . . . . . . . . . . . . 17 (x Nn → ( ≤c We NCm NC ( Nc ( Spacm) = (1c +c x) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))))
245 fveq2 5328 . . . . . . . . . . . . . . . . . . . . 21 (m = M → ( Spacm) = ( SpacM))
246245nceqd 6110 . . . . . . . . . . . . . . . . . . . 20 (m = MNc ( Spacm) = Nc ( SpacM))
247246eqeq1d 2361 . . . . . . . . . . . . . . . . . . 19 (m = M → ( Nc ( Spacm) = (1c +c x) ↔ Nc ( SpacM) = (1c +c x)))
248 tceq 6158 . . . . . . . . . . . . . . . . . . . . . 22 (m = MTc m = Tc M)
249248fveq2d 5332 . . . . . . . . . . . . . . . . . . . . 21 (m = M → ( SpacTc m) = ( SpacTc M))
250249eleq1d 2419 . . . . . . . . . . . . . . . . . . . 20 (m = M → (( SpacTc m) Fin ↔ ( SpacTc M) Fin ))
251249nceqd 6110 . . . . . . . . . . . . . . . . . . . . . 22 (m = MNc ( SpacTc m) = Nc ( SpacTc M))
252 tceq 6158 . . . . . . . . . . . . . . . . . . . . . . . 24 ( Nc ( Spacm) = Nc ( SpacM) → Tc Nc ( Spacm) = Tc Nc ( SpacM))
253246, 252syl 15 . . . . . . . . . . . . . . . . . . . . . . 23 (m = MTc Nc ( Spacm) = Tc Nc ( SpacM))
254253addceq1d 4389 . . . . . . . . . . . . . . . . . . . . . 22 (m = M → ( Tc Nc ( Spacm) +c 1c) = ( Tc Nc ( SpacM) +c 1c))
255251, 254eqeq12d 2367 . . . . . . . . . . . . . . . . . . . . 21 (m = M → ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) ↔ Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 1c)))
256253addceq1d 4389 . . . . . . . . . . . . . . . . . . . . . 22 (m = M → ( Tc Nc ( Spacm) +c 2c) = ( Tc Nc ( SpacM) +c 2c))
257251, 256eqeq12d 2367 . . . . . . . . . . . . . . . . . . . . 21 (m = M → ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c) ↔ Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 2c)))
258255, 257orbi12d 690 . . . . . . . . . . . . . . . . . . . 20 (m = M → (( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)) ↔ ( Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 1c) Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 2c))))
259250, 258anbi12d 691 . . . . . . . . . . . . . . . . . . 19 (m = M → ((( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))) ↔ (( SpacTc M) Fin ( Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 1c) Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 2c)))))
260247, 259imbi12d 311 . . . . . . . . . . . . . . . . . 18 (m = M → (( Nc ( Spacm) = (1c +c x) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) ↔ ( Nc ( SpacM) = (1c +c x) → (( SpacTc M) Fin ( Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 1c) Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 2c))))))
261260rspccv 2952 . . . . . . . . . . . . . . . . 17 (m NC ( Nc ( Spacm) = (1c +c x) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))) → (M NC → ( Nc ( SpacM) = (1c +c x) → (( SpacTc M) Fin ( Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 1c) Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 2c))))))
262244, 261syl6com 31 . . . . . . . . . . . . . . . 16 ( ≤c We NC → (x Nn → (M NC → ( Nc ( SpacM) = (1c +c x) → (( SpacTc M) Fin ( Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 1c) Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 2c)))))))
263262com23 72 . . . . . . . . . . . . . . 15 ( ≤c We NC → (M NC → (x Nn → ( Nc ( SpacM) = (1c +c x) → (( SpacTc M) Fin ( Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 1c) Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 2c)))))))
264263imp 418 . . . . . . . . . . . . . 14 (( ≤c We NC M NC ) → (x Nn → ( Nc ( SpacM) = (1c +c x) → (( SpacTc M) Fin ( Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 1c) Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 2c))))))
265264adantr 451 . . . . . . . . . . . . 13 ((( ≤c We NC M NC ) t Nn ) → (x Nn → ( Nc ( SpacM) = (1c +c x) → (( SpacTc M) Fin ( Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 1c) Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 2c))))))
266265adantr 451 . . . . . . . . . . . 12 (((( ≤c We NC M NC ) t Nn ) x NC ) → (x Nn → ( Nc ( SpacM) = (1c +c x) → (( SpacTc M) Fin ( Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 1c) Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 2c))))))
26727, 31, 2663syld 51 . . . . . . . . . . 11 (((( ≤c We NC M NC ) t Nn ) x NC ) → (t = (1c +c x) → ( Nc ( SpacM) = (1c +c x) → (( SpacTc M) Fin ( Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 1c) Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 2c))))))
268267imp3a 420 . . . . . . . . . 10 (((( ≤c We NC M NC ) t Nn ) x NC ) → ((t = (1c +c x) Nc ( SpacM) = (1c +c x)) → (( SpacTc M) Fin ( Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 1c) Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 2c)))))
26915, 268syl5 28 . . . . . . . . 9 (((( ≤c We NC M NC ) t Nn ) x NC ) → (( Nc ( SpacM) = (1c +c x) t = Nc ( SpacM)) → (( SpacTc M) Fin ( Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 1c) Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 2c)))))
270269exp3a 425 . . . . . . . 8 (((( ≤c We NC M NC ) t Nn ) x NC ) → ( Nc ( SpacM) = (1c +c x) → (t = Nc ( SpacM) → (( SpacTc M) Fin ( Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 1c) Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 2c))))))
271270rexlimdva 2738 . . . . . . 7 ((( ≤c We NC M NC ) t Nn ) → (x NC Nc ( SpacM) = (1c +c x) → (t = Nc ( SpacM) → (( SpacTc M) Fin ( Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 1c) Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 2c))))))
2729, 271syl5bi 208 . . . . . 6 ((( ≤c We NC M NC ) t Nn ) → (1cc Nc ( SpacM) → (t = Nc ( SpacM) → (( SpacTc M) Fin ( Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 1c) Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 2c))))))
2734, 272mpd 14 . . . . 5 ((( ≤c We NC M NC ) t Nn ) → (t = Nc ( SpacM) → (( SpacTc M) Fin ( Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 1c) Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 2c)))))
274273rexlimdva 2738 . . . 4 (( ≤c We NC M NC ) → (t Nn t = Nc ( SpacM) → (( SpacTc M) Fin ( Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 1c) Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 2c)))))
2752, 274syl5bi 208 . . 3 (( ≤c We NC M NC ) → ( Nc ( SpacM) Nn → (( SpacTc M) Fin ( Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 1c) Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 2c)))))
2761, 275syl5bi 208 . 2 (( ≤c We NC M NC ) → (( SpacM) Fin → (( SpacTc M) Fin ( Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 1c) Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 2c)))))
2772763impia 1148 1 (( ≤c We NC M NC ( SpacM) Fin ) → (( SpacTc M) Fin ( Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 1c) Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 2c))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 176   wo 357   wa 358   w3a 934   = wceq 1642   wcel 1710  wne 2516  wral 2614  wrex 2615  {csn 3737  1cc1c 4134   Nn cnnc 4373  0cc0c 4374   +c cplc 4375   Fin cfin 4376   class class class wbr 4639  cfv 4781  (class class class)co 5525   We cwe 5895   NC cncs 6088  c clec 6089   <c cltc 6090   Nc cnc 6091   Tc ctc 6093  2cc2c 6094  3cc3c 6095  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-csb 3137  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-tp 3743  df-uni 3892  df-int 3927  df-iun 3971  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-cup 5742  df-disj 5744  df-addcfn 5746  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-antisym 5901  df-partial 5902  df-connex 5903  df-strict 5904  df-we 5906  df-sym 5908  df-er 5909  df-ec 5947  df-qs 5951  df-map 6001  df-en 6029  df-ncs 6098  df-lec 6099  df-ltc 6100  df-nc 6101  df-tc 6103  df-2c 6104  df-3c 6105  df-ce 6106  df-tcfn 6107  df-spac 6274
This theorem is referenced by:  nchoicelem19  6307  nchoice  6308
  Copyright terms: Public domain W3C validator