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

Theorem nchoicelem19 6307
 Description: Lemma for nchoice 6308. Assuming well-ordering, there is a cardinal with a finite special set that is its own T-raising. Theorem 7.3 of [Specker] p. 974. (Contributed by SF, 20-Mar-2015.)
Assertion
Ref Expression
nchoicelem19 ( ≤c We NCm NC (( Spacm) Fin Tc m = m))

Proof of Theorem nchoicelem19
Dummy variables n x p are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nchoicelem18 6306 . . 3 {x ( Spacx) Fin } V
2 fveq2 5328 . . . 4 (x = m → ( Spacx) = ( Spacm))
32eleq1d 2419 . . 3 (x = m → (( Spacx) Fin ↔ ( Spacm) Fin ))
4 fveq2 5328 . . . 4 (x = n → ( Spacx) = ( Spacn))
54eleq1d 2419 . . 3 (x = n → (( Spacx) Fin ↔ ( Spacn) Fin ))
6 id 19 . . 3 ( ≤c We NC → ≤c We NC )
7 vvex 4109 . . . . 5 V V
87ncelncsi 6121 . . . 4 Nc V NC
9 ltcpw1pwg 6202 . . . . . . . . 9 (V V → Nc 1V <c Nc V)
107, 9ax-mp 5 . . . . . . . 8 Nc 1V <c Nc V
11 df1c2 4168 . . . . . . . . 9 1c = 1V
1211nceqi 6109 . . . . . . . 8 Nc 1c = Nc 1V
13 pwv 3886 . . . . . . . . . 10 V = V
1413nceqi 6109 . . . . . . . . 9 Nc V = Nc V
1514eqcomi 2357 . . . . . . . 8 Nc V = Nc V
1610, 12, 153brtr4i 4667 . . . . . . 7 Nc 1c <c Nc V
17 nchoicelem8 6296 . . . . . . . 8 (( ≤c We NC Nc V NC ) → (¬ ( Nc V ↑c 0c) NCNc 1c <c Nc V))
188, 17mpan2 652 . . . . . . 7 ( ≤c We NC → (¬ ( Nc V ↑c 0c) NCNc 1c <c Nc V))
1916, 18mpbiri 224 . . . . . 6 ( ≤c We NC → ¬ ( Nc V ↑c 0c) NC )
20 nchoicelem3 6291 . . . . . 6 (( Nc V NC ¬ ( Nc V ↑c 0c) NC ) → ( SpacNc V) = { Nc V})
218, 19, 20sylancr 644 . . . . 5 ( ≤c We NC → ( SpacNc V) = { Nc V})
22 snfi 4431 . . . . 5 { Nc V} Fin
2321, 22syl6eqel 2441 . . . 4 ( ≤c We NC → ( SpacNc V) Fin )
24 fveq2 5328 . . . . . 6 (x = Nc V → ( Spacx) = ( SpacNc V))
2524eleq1d 2419 . . . . 5 (x = Nc V → (( Spacx) Fin ↔ ( SpacNc V) Fin ))
2625rspcev 2955 . . . 4 (( Nc V NC ( SpacNc V) Fin ) → x NC ( Spacx) Fin )
278, 23, 26sylancr 644 . . 3 ( ≤c We NCx NC ( Spacx) Fin )
281, 3, 5, 6, 27weds 5938 . 2 ( ≤c We NCm NC (( Spacm) Fin n NC (( Spacn) Finmc n)))
29 simpll 730 . . . . . . 7 ((( ≤c We NC m NC ) (( Spacm) Fin n NC (( Spacn) Finmc n))) → ≤c We NC )
30 df-we 5906 . . . . . . . . . . 11 We = ( OrFr )
3130breqi 4645 . . . . . . . . . 10 ( ≤c We NC ↔ ≤c ( OrFr ) NC )
32 brin 4693 . . . . . . . . . 10 ( ≤c ( OrFr ) NC ↔ ( ≤c Or NC c Fr NC ))
3331, 32bitri 240 . . . . . . . . 9 ( ≤c We NC ↔ ( ≤c Or NC c Fr NC ))
3433simplbi 446 . . . . . . . 8 ( ≤c We NC → ≤c Or NC )
35 sopc 5934 . . . . . . . . . 10 ( ≤c Or NC ↔ ( ≤c Po NC c Connex NC ))
3635simplbi 446 . . . . . . . . 9 ( ≤c Or NC → ≤c Po NC )
37 porta 5933 . . . . . . . . . 10 ( ≤c Po NC ↔ ( ≤c Ref NC c Trans NC c Antisym NC ))
3837simp3bi 972 . . . . . . . . 9 ( ≤c Po NC → ≤c Antisym NC )
3936, 38syl 15 . . . . . . . 8 ( ≤c Or NC → ≤c Antisym NC )
4034, 39syl 15 . . . . . . 7 ( ≤c We NC → ≤c Antisym NC )
4129, 40syl 15 . . . . . 6 ((( ≤c We NC m NC ) (( Spacm) Fin n NC (( Spacn) Finmc n))) → ≤c Antisym NC )
42 simplr 731 . . . . . . 7 ((( ≤c We NC m NC ) (( Spacm) Fin n NC (( Spacn) Finmc n))) → m NC )
43 tccl 6160 . . . . . . 7 (m NCTc m NC )
4442, 43syl 15 . . . . . 6 ((( ≤c We NC m NC ) (( Spacm) Fin n NC (( Spacn) Finmc n))) → Tc m NC )
45 simprr 733 . . . . . . . 8 ((( ≤c We NC m NC ) (( Spacm) Fin n NC (( Spacn) Finmc n))) → n NC (( Spacn) Finmc n))
46 simprl 732 . . . . . . . . . 10 ((( ≤c We NC m NC ) (( Spacm) Fin n NC (( Spacn) Finmc n))) → ( Spacm) Fin )
47 nchoicelem17 6305 . . . . . . . . . 10 (( ≤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))))
4829, 42, 46, 47syl3anc 1182 . . . . . . . . 9 ((( ≤c We NC m NC ) (( Spacm) Fin n NC (( Spacn) Finmc n))) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))
4948simpld 445 . . . . . . . 8 ((( ≤c We NC m NC ) (( Spacm) Fin n NC (( Spacn) Finmc n))) → ( SpacTc m) Fin )
50 fveq2 5328 . . . . . . . . . . 11 (n = Tc m → ( Spacn) = ( SpacTc m))
5150eleq1d 2419 . . . . . . . . . 10 (n = Tc m → (( Spacn) Fin ↔ ( SpacTc m) Fin ))
52 breq2 4643 . . . . . . . . . 10 (n = Tc m → (mc nmc Tc m))
5351, 52imbi12d 311 . . . . . . . . 9 (n = Tc m → ((( Spacn) Finmc n) ↔ (( SpacTc m) Finmc Tc m)))
5453rspcv 2951 . . . . . . . 8 ( Tc m NC → (n NC (( Spacn) Finmc n) → (( SpacTc m) Finmc Tc m)))
5544, 45, 49, 54syl3c 57 . . . . . . 7 ((( ≤c We NC m NC ) (( Spacm) Fin n NC (( Spacn) Finmc n))) → mc Tc m)
56 letc 6231 . . . . . . . . . 10 ((m NC m NC mc Tc m) → p NC m = Tc p)
57563expia 1153 . . . . . . . . 9 ((m NC m NC ) → (mc Tc mp NC m = Tc p))
5842, 42, 57syl2anc 642 . . . . . . . 8 ((( ≤c We NC m NC ) (( Spacm) Fin n NC (( Spacn) Finmc n))) → (mc Tc mp NC m = Tc p))
59 nchoicelem12 6300 . . . . . . . . . . . . . . . 16 ((p NC ( SpacTc p) Fin ) → ( Spacp) Fin )
6059ad2ant2lr 728 . . . . . . . . . . . . . . 15 ((( ≤c We NC p NC ) (( SpacTc p) Fin n NC (( Spacn) FinTc pc n))) → ( Spacp) Fin )
61 fveq2 5328 . . . . . . . . . . . . . . . . . . . 20 (n = p → ( Spacn) = ( Spacp))
6261eleq1d 2419 . . . . . . . . . . . . . . . . . . 19 (n = p → (( Spacn) Fin ↔ ( Spacp) Fin ))
63 breq2 4643 . . . . . . . . . . . . . . . . . . 19 (n = p → ( Tc pc nTc pc p))
6462, 63imbi12d 311 . . . . . . . . . . . . . . . . . 18 (n = p → ((( Spacn) FinTc pc n) ↔ (( Spacp) FinTc pc p)))
6564rspcv 2951 . . . . . . . . . . . . . . . . 17 (p NC → (n NC (( Spacn) FinTc pc n) → (( Spacp) FinTc pc p)))
6665imp 418 . . . . . . . . . . . . . . . 16 ((p NC n NC (( Spacn) FinTc pc n)) → (( Spacp) FinTc pc p))
6766ad2ant2l 726 . . . . . . . . . . . . . . 15 ((( ≤c We NC p NC ) (( SpacTc p) Fin n NC (( Spacn) FinTc pc n))) → (( Spacp) FinTc pc p))
6860, 67mpd 14 . . . . . . . . . . . . . 14 ((( ≤c We NC p NC ) (( SpacTc p) Fin n NC (( Spacn) FinTc pc n))) → Tc pc p)
69 simplr 731 . . . . . . . . . . . . . . . 16 ((( ≤c We NC p NC ) (( SpacTc p) Fin n NC (( Spacn) FinTc pc n))) → p NC )
70 tccl 6160 . . . . . . . . . . . . . . . 16 (p NCTc p NC )
7169, 70syl 15 . . . . . . . . . . . . . . 15 ((( ≤c We NC p NC ) (( SpacTc p) Fin n NC (( Spacn) FinTc pc n))) → Tc p NC )
72 tlecg 6230 . . . . . . . . . . . . . . 15 (( Tc p NC p NC ) → ( Tc pc pTc Tc pc Tc p))
7371, 69, 72syl2anc 642 . . . . . . . . . . . . . 14 ((( ≤c We NC p NC ) (( SpacTc p) Fin n NC (( Spacn) FinTc pc n))) → ( Tc pc pTc Tc pc Tc p))
7468, 73mpbid 201 . . . . . . . . . . . . 13 ((( ≤c We NC p NC ) (( SpacTc p) Fin n NC (( Spacn) FinTc pc n))) → Tc Tc pc Tc p)
75 fveq2 5328 . . . . . . . . . . . . . . . . 17 (m = Tc p → ( Spacm) = ( SpacTc p))
7675eleq1d 2419 . . . . . . . . . . . . . . . 16 (m = Tc p → (( Spacm) Fin ↔ ( SpacTc p) Fin ))
77 breq1 4642 . . . . . . . . . . . . . . . . . 18 (m = Tc p → (mc nTc pc n))
7877imbi2d 307 . . . . . . . . . . . . . . . . 17 (m = Tc p → ((( Spacn) Finmc n) ↔ (( Spacn) FinTc pc n)))
7978ralbidv 2634 . . . . . . . . . . . . . . . 16 (m = Tc p → (n NC (( Spacn) Finmc n) ↔ n NC (( Spacn) FinTc pc n)))
8076, 79anbi12d 691 . . . . . . . . . . . . . . 15 (m = Tc p → ((( Spacm) Fin n NC (( Spacn) Finmc n)) ↔ (( SpacTc p) Fin n NC (( Spacn) FinTc pc n))))
8180anbi2d 684 . . . . . . . . . . . . . 14 (m = Tc p → ((( ≤c We NC p NC ) (( Spacm) Fin n NC (( Spacn) Finmc n))) ↔ (( ≤c We NC p NC ) (( SpacTc p) Fin n NC (( Spacn) FinTc pc n)))))
82 tceq 6158 . . . . . . . . . . . . . . 15 (m = Tc pTc m = Tc Tc p)
83 id 19 . . . . . . . . . . . . . . 15 (m = Tc pm = Tc p)
8482, 83breq12d 4652 . . . . . . . . . . . . . 14 (m = Tc p → ( Tc mc mTc Tc pc Tc p))
8581, 84imbi12d 311 . . . . . . . . . . . . 13 (m = Tc p → (((( ≤c We NC p NC ) (( Spacm) Fin n NC (( Spacn) Finmc n))) → Tc mc m) ↔ ((( ≤c We NC p NC ) (( SpacTc p) Fin n NC (( Spacn) FinTc pc n))) → Tc Tc pc Tc p)))
8674, 85mpbiri 224 . . . . . . . . . . . 12 (m = Tc p → ((( ≤c We NC p NC ) (( Spacm) Fin n NC (( Spacn) Finmc n))) → Tc mc m))
8786com12 27 . . . . . . . . . . 11 ((( ≤c We NC p NC ) (( Spacm) Fin n NC (( Spacn) Finmc n))) → (m = Tc pTc mc m))
8887an32s 779 . . . . . . . . . 10 ((( ≤c We NC (( Spacm) Fin n NC (( Spacn) Finmc n))) p NC ) → (m = Tc pTc mc m))
8988rexlimdva 2738 . . . . . . . . 9 (( ≤c We NC (( Spacm) Fin n NC (( Spacn) Finmc n))) → (p NC m = Tc pTc mc m))
9089adantlr 695 . . . . . . . 8 ((( ≤c We NC m NC ) (( Spacm) Fin n NC (( Spacn) Finmc n))) → (p NC m = Tc pTc mc m))
9158, 90syld 40 . . . . . . 7 ((( ≤c We NC m NC ) (( Spacm) Fin n NC (( Spacn) Finmc n))) → (mc Tc mTc mc m))
9255, 91mpd 14 . . . . . 6 ((( ≤c We NC m NC ) (( Spacm) Fin n NC (( Spacn) Finmc n))) → Tc mc m)
9341, 44, 42, 92, 55antid 5929 . . . . 5 ((( ≤c We NC m NC ) (( Spacm) Fin n NC (( Spacn) Finmc n))) → Tc m = m)
9493exp32 588 . . . 4 (( ≤c We NC m NC ) → (( Spacm) Fin → (n NC (( Spacn) Finmc n) → Tc m = m)))
9594imdistand 673 . . 3 (( ≤c We NC m NC ) → ((( Spacm) Fin n NC (( Spacn) Finmc n)) → (( Spacm) Fin Tc m = m)))
9695reximdva 2726 . 2 ( ≤c We NC → (m NC (( Spacm) Fin n NC (( Spacn) Finmc n)) → m NC (( Spacm) Fin Tc m = m)))
9728, 96mpd 14 1 ( ≤c We NCm NC (( Spacm) Fin Tc m = m))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∨ wo 357   ∧ wa 358   = wceq 1642   ∈ wcel 1710  ∀wral 2614  ∃wrex 2615  Vcvv 2859   ∩ cin 3208  ℘cpw 3722  {csn 3737  1cc1c 4134  ℘1cpw1 4135  0cc0c 4374   +c cplc 4375   Fin cfin 4376   class class class wbr 4639   ‘cfv 4781  (class class class)co 5525   Trans ctrans 5888   Ref cref 5889   Antisym cantisym 5890   Po cpartial 5891   Connex cconnex 5892   Or cstrict 5893   Fr cfound 5894   We cwe 5895   NC cncs 6088   ≤c clec 6089
 Copyright terms: Public domain W3C validator