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

Theorem vfin1cltv 4547
 Description: If the universe is finite, then 1c is strictly smaller than the universe. Theorem X.1.57 of [Rosser] p. 534. (Contributed by SF, 30-Jan-2015.)
Assertion
Ref Expression
vfin1cltv (V Fin → ⟪ Ncfin 1c, Ncfin V⟫ <fin )

Proof of Theorem vfin1cltv
StepHypRef Expression
1 uncompl 4074 . . . . 5 (1c ∪ ∼ 1c) = V
2 ncfineq 4473 . . . . 5 ((1c ∪ ∼ 1c) = V → Ncfin (1c ∪ ∼ 1c) = Ncfin V)
31, 2ax-mp 8 . . . 4 Ncfin (1c ∪ ∼ 1c) = Ncfin V
4 1cex 4142 . . . . 5 1c V
54complex 4104 . . . . . 6 ∼ 1c V
6 incompl 4073 . . . . . 6 (1c ∩ ∼ 1c) =
7 ncfindi 4475 . . . . . 6 (((V Fin 1c V) ∼ 1c V (1c ∩ ∼ 1c) = ) → Ncfin (1c ∪ ∼ 1c) = ( Ncfin 1c +c Ncfin ∼ 1c))
85, 6, 7mp3an23 1269 . . . . 5 ((V Fin 1c V) → Ncfin (1c ∪ ∼ 1c) = ( Ncfin 1c +c Ncfin ∼ 1c))
94, 8mpan2 652 . . . 4 (V FinNcfin (1c ∪ ∼ 1c) = ( Ncfin 1c +c Ncfin ∼ 1c))
103, 9syl5reqr 2400 . . 3 (V Fin → ( Ncfin 1c +c Ncfin ∼ 1c) = Ncfin V)
1110opkeq2d 4066 . 2 (V Fin → ⟪ Ncfin 1c, ( Ncfin 1c +c Ncfin ∼ 1c)⟫ = ⟪ Ncfin 1c, Ncfin V⟫)
12 0nel1c 4159 . . . . . . 7 ¬ 1c
13 0ex 4110 . . . . . . . 8 V
1413elcompl 3225 . . . . . . 7 ( ∼ 1c ↔ ¬ 1c)
1512, 14mpbir 200 . . . . . 6 ∼ 1c
16 n0i 3555 . . . . . 6 ( ∼ 1c → ¬ ∼ 1c = )
1715, 16ax-mp 8 . . . . 5 ¬ ∼ 1c =
18 ncfinprop 4474 . . . . . . . . 9 ((V Fin ∼ 1c V) → ( Ncfin ∼ 1c Nn ∼ 1c Ncfin ∼ 1c))
195, 18mpan2 652 . . . . . . . 8 (V Fin → ( Ncfin ∼ 1c Nn ∼ 1c Ncfin ∼ 1c))
2019simprd 449 . . . . . . 7 (V Fin → ∼ 1c Ncfin ∼ 1c)
21 eleq2 2414 . . . . . . 7 (0c = Ncfin ∼ 1c → ( ∼ 1c 0c ↔ ∼ 1c Ncfin ∼ 1c))
2220, 21syl5ibrcom 213 . . . . . 6 (V Fin → (0c = Ncfin ∼ 1c → ∼ 1c 0c))
23 el0c 4421 . . . . . 6 ( ∼ 1c 0c ↔ ∼ 1c = )
2422, 23syl6ib 217 . . . . 5 (V Fin → (0c = Ncfin ∼ 1c → ∼ 1c = ))
2517, 24mtoi 169 . . . 4 (V Fin → ¬ 0c = Ncfin ∼ 1c)
26 addcid1 4405 . . . . . 6 ( Ncfin 1c +c 0c) = Ncfin 1c
2726eqeq1i 2360 . . . . 5 (( Ncfin 1c +c 0c) = ( Ncfin 1c +c Ncfin ∼ 1c) ↔ Ncfin 1c = ( Ncfin 1c +c Ncfin ∼ 1c))
28 ncfinprop 4474 . . . . . . . 8 ((V Fin 1c V) → ( Ncfin 1c Nn 1c Ncfin 1c))
294, 28mpan2 652 . . . . . . 7 (V Fin → ( Ncfin 1c Nn 1c Ncfin 1c))
3029simpld 445 . . . . . 6 (V FinNcfin 1c Nn )
31 peano1 4402 . . . . . . 7 0c Nn
3231a1i 10 . . . . . 6 (V Fin → 0c Nn )
3319simpld 445 . . . . . 6 (V FinNcfin ∼ 1c Nn )
3426a1i 10 . . . . . . 7 (V Fin → ( Ncfin 1c +c 0c) = Ncfin 1c)
3529simprd 449 . . . . . . . 8 (V Fin → 1c Ncfin 1c)
36 ne0i 3556 . . . . . . . 8 (1c Ncfin 1cNcfin 1c)
3735, 36syl 15 . . . . . . 7 (V FinNcfin 1c)
3834, 37eqnetrd 2534 . . . . . 6 (V Fin → ( Ncfin 1c +c 0c) ≠ )
39 preaddccan2 4455 . . . . . 6 ((( Ncfin 1c Nn 0c Nn Ncfin ∼ 1c Nn ) ( Ncfin 1c +c 0c) ≠ ) → (( Ncfin 1c +c 0c) = ( Ncfin 1c +c Ncfin ∼ 1c) ↔ 0c = Ncfin ∼ 1c))
4030, 32, 33, 38, 39syl31anc 1185 . . . . 5 (V Fin → (( Ncfin 1c +c 0c) = ( Ncfin 1c +c Ncfin ∼ 1c) ↔ 0c = Ncfin ∼ 1c))
4127, 40syl5bbr 250 . . . 4 (V Fin → ( Ncfin 1c = ( Ncfin 1c +c Ncfin ∼ 1c) ↔ 0c = Ncfin ∼ 1c))
4225, 41mtbird 292 . . 3 (V Fin → ¬ Ncfin 1c = ( Ncfin 1c +c Ncfin ∼ 1c))
43 ncfinex 4472 . . . . . . 7 Ncfin 1c V
44 lefinaddc 4450 . . . . . . 7 (( Ncfin 1c V Ncfin ∼ 1c Nn ) → ⟪ Ncfin 1c, ( Ncfin 1c +c Ncfin ∼ 1c)⟫ fin )
4543, 33, 44sylancr 644 . . . . . 6 (V Fin → ⟪ Ncfin 1c, ( Ncfin 1c +c Ncfin ∼ 1c)⟫ fin )
46 ncfinex 4472 . . . . . . . . 9 Ncfin ∼ 1c V
4743, 46addcex 4394 . . . . . . . 8 ( Ncfin 1c +c Ncfin ∼ 1c) V
48 lefinlteq 4463 . . . . . . . 8 (( Ncfin 1c V ( Ncfin 1c +c Ncfin ∼ 1c) V Ncfin 1c) → (⟪ Ncfin 1c, ( Ncfin 1c +c Ncfin ∼ 1c)⟫ fin ↔ (⟪ Ncfin 1c, ( Ncfin 1c +c Ncfin ∼ 1c)⟫ <fin Ncfin 1c = ( Ncfin 1c +c Ncfin ∼ 1c))))
4943, 47, 48mp3an12 1267 . . . . . . 7 ( Ncfin 1c → (⟪ Ncfin 1c, ( Ncfin 1c +c Ncfin ∼ 1c)⟫ fin ↔ (⟪ Ncfin 1c, ( Ncfin 1c +c Ncfin ∼ 1c)⟫ <fin Ncfin 1c = ( Ncfin 1c +c Ncfin ∼ 1c))))
5037, 49syl 15 . . . . . 6 (V Fin → (⟪ Ncfin 1c, ( Ncfin 1c +c Ncfin ∼ 1c)⟫ fin ↔ (⟪ Ncfin 1c, ( Ncfin 1c +c Ncfin ∼ 1c)⟫ <fin Ncfin 1c = ( Ncfin 1c +c Ncfin ∼ 1c))))
5145, 50mpbid 201 . . . . 5 (V Fin → (⟪ Ncfin 1c, ( Ncfin 1c +c Ncfin ∼ 1c)⟫ <fin Ncfin 1c = ( Ncfin 1c +c Ncfin ∼ 1c)))
5251orcomd 377 . . . 4 (V Fin → ( Ncfin 1c = ( Ncfin 1c +c Ncfin ∼ 1c) Ncfin 1c, ( Ncfin 1c +c Ncfin ∼ 1c)⟫ <fin ))
5352ord 366 . . 3 (V Fin → (¬ Ncfin 1c = ( Ncfin 1c +c Ncfin ∼ 1c) → ⟪ Ncfin 1c, ( Ncfin 1c +c Ncfin ∼ 1c)⟫ <fin ))
5442, 53mpd 14 . 2 (V Fin → ⟪ Ncfin 1c, ( Ncfin 1c +c Ncfin ∼ 1c)⟫ <fin )
5511, 54eqeltrrd 2428 1 (V Fin → ⟪ Ncfin 1c, Ncfin V⟫ <fin )
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∨ wo 357   ∧ wa 358   = wceq 1642   ∈ wcel 1710   ≠ wne 2516  Vcvv 2859   ∼ ccompl 3205   ∪ cun 3207   ∩ cin 3208  ∅c0 3550  ⟪copk 4057  1cc1c 4134   Nn cnnc 4373  0cc0c 4374   +c cplc 4375   Fin cfin 4376   ≤fin clefin 4432
 Copyright terms: Public domain W3C validator