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

Theorem nchoicelem8 6296
 Description: Lemma for nchoice 6308. An anti-closure condition for cardinal exponentiation to zero. Theorem 4.5 of [Specker] p. 973. (Contributed by SF, 18-Mar-2015.)
Assertion
Ref Expression
nchoicelem8 (( ≤c We NC M NC ) → (¬ (Mc 0c) NCNc 1c <c M))

Proof of Theorem nchoicelem8
StepHypRef Expression
1 ce0lenc1 6239 . . . 4 (M NC → ((Mc 0c) NCMc Nc 1c))
21notbid 285 . . 3 (M NC → (¬ (Mc 0c) NC ↔ ¬ Mc Nc 1c))
32adantl 452 . 2 (( ≤c We NC M NC ) → (¬ (Mc 0c) NC ↔ ¬ Mc Nc 1c))
4 df-we 5906 . . . . . . . . . 10 We = ( OrFr )
54breqi 4645 . . . . . . . . 9 ( ≤c We NC ↔ ≤c ( OrFr ) NC )
6 brin 4693 . . . . . . . . 9 ( ≤c ( OrFr ) NC ↔ ( ≤c Or NC c Fr NC ))
75, 6bitri 240 . . . . . . . 8 ( ≤c We NC ↔ ( ≤c Or NC c Fr NC ))
8 sopc 5934 . . . . . . . . . 10 ( ≤c Or NC ↔ ( ≤c Po NC c Connex NC ))
98simprbi 450 . . . . . . . . 9 ( ≤c Or NC → ≤c Connex NC )
109adantr 451 . . . . . . . 8 (( ≤c Or NC c Fr NC ) → ≤c Connex NC )
117, 10sylbi 187 . . . . . . 7 ( ≤c We NC → ≤c Connex NC )
12 simpl 443 . . . . . . . 8 (( ≤c Connex NC M NC ) → ≤c Connex NC )
13 simpr 447 . . . . . . . 8 (( ≤c Connex NC M NC ) → M NC )
14 1cex 4142 . . . . . . . . . 10 1c V
1514ncelncsi 6121 . . . . . . . . 9 Nc 1c NC
1615a1i 10 . . . . . . . 8 (( ≤c Connex NC M NC ) → Nc 1c NC )
1712, 13, 16connexd 5931 . . . . . . 7 (( ≤c Connex NC M NC ) → (Mc Nc 1c Nc 1cc M))
1811, 17sylan 457 . . . . . 6 (( ≤c We NC M NC ) → (Mc Nc 1c Nc 1cc M))
1918ord 366 . . . . 5 (( ≤c We NC M NC ) → (¬ Mc Nc 1cNc 1cc M))
20 id 19 . . . . . . . 8 ( Nc 1c = MNc 1c = M)
21 nclecid 6197 . . . . . . . . 9 ( Nc 1c NCNc 1cc Nc 1c)
2215, 21ax-mp 8 . . . . . . . 8 Nc 1cc Nc 1c
2320, 22syl6eqbrr 4677 . . . . . . 7 ( Nc 1c = MMc Nc 1c)
2423necon3bi 2557 . . . . . 6 Mc Nc 1cNc 1cM)
2524a1i 10 . . . . 5 (( ≤c We NC M NC ) → (¬ Mc Nc 1cNc 1cM))
2619, 25jcad 519 . . . 4 (( ≤c We NC M NC ) → (¬ Mc Nc 1c → ( Nc 1cc M Nc 1cM)))
277simplbi 446 . . . . . . . . . . 11 ( ≤c We NC → ≤c Or NC )
288simplbi 446 . . . . . . . . . . 11 ( ≤c Or NC → ≤c Po NC )
29 df-partial 5902 . . . . . . . . . . . . . 14 Po = (( RefTrans ) ∩ Antisym )
3029breqi 4645 . . . . . . . . . . . . 13 ( ≤c Po NC ↔ ≤c (( RefTrans ) ∩ Antisym ) NC )
31 brin 4693 . . . . . . . . . . . . 13 ( ≤c (( RefTrans ) ∩ Antisym ) NC ↔ ( ≤c ( RefTrans ) NC c Antisym NC ))
3230, 31bitri 240 . . . . . . . . . . . 12 ( ≤c Po NC ↔ ( ≤c ( RefTrans ) NC c Antisym NC ))
3332simprbi 450 . . . . . . . . . . 11 ( ≤c Po NC → ≤c Antisym NC )
3427, 28, 333syl 18 . . . . . . . . . 10 ( ≤c We NC → ≤c Antisym NC )
3534adantr 451 . . . . . . . . 9 (( ≤c We NC M NC ) → ≤c Antisym NC )
3635adantr 451 . . . . . . . 8 ((( ≤c We NC M NC ) ( Nc 1cc M Mc Nc 1c)) → ≤c Antisym NC )
3715a1i 10 . . . . . . . 8 ((( ≤c We NC M NC ) ( Nc 1cc M Mc Nc 1c)) → Nc 1c NC )
38 simplr 731 . . . . . . . 8 ((( ≤c We NC M NC ) ( Nc 1cc M Mc Nc 1c)) → M NC )
39 simprl 732 . . . . . . . 8 ((( ≤c We NC M NC ) ( Nc 1cc M Mc Nc 1c)) → Nc 1cc M)
40 simprr 733 . . . . . . . 8 ((( ≤c We NC M NC ) ( Nc 1cc M Mc Nc 1c)) → Mc Nc 1c)
4136, 37, 38, 39, 40antid 5929 . . . . . . 7 ((( ≤c We NC M NC ) ( Nc 1cc M Mc Nc 1c)) → Nc 1c = M)
4241expr 598 . . . . . 6 ((( ≤c We NC M NC ) Nc 1cc M) → (Mc Nc 1cNc 1c = M))
4342necon3ad 2552 . . . . 5 ((( ≤c We NC M NC ) Nc 1cc M) → ( Nc 1cM → ¬ Mc Nc 1c))
4443expimpd 586 . . . 4 (( ≤c We NC M NC ) → (( Nc 1cc M Nc 1cM) → ¬ Mc Nc 1c))
4526, 44impbid 183 . . 3 (( ≤c We NC M NC ) → (¬ Mc Nc 1c ↔ ( Nc 1cc M Nc 1cM)))
46 brltc 6114 . . 3 ( Nc 1c <c M ↔ ( Nc 1cc M Nc 1cM))
4745, 46syl6bbr 254 . 2 (( ≤c We NC M NC ) → (¬ Mc Nc 1cNc 1c <c M))
483, 47bitrd 244 1 (( ≤c We NC M NC ) → (¬ (Mc 0c) NCNc 1c <c M))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∨ wo 357   ∧ wa 358   = wceq 1642   ∈ wcel 1710   ≠ wne 2516   ∩ cin 3208  1cc1c 4134  0cc0c 4374   class class class wbr 4639  (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