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

Theorem ltlefin 4468
 Description: Less than implies less than or equal. (Contributed by SF, 2-Feb-2015.)
Assertion
Ref Expression
ltlefin ((A V B W) → (⟪A, B <fin → ⟪A, Bfin ))

Proof of Theorem ltlefin
Dummy variables x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 addcass 4415 . . . . . . 7 ((A +c x) +c 1c) = (A +c (x +c 1c))
21eqeq2i 2363 . . . . . 6 (B = ((A +c x) +c 1c) ↔ B = (A +c (x +c 1c)))
3 peano2 4403 . . . . . . 7 (x Nn → (x +c 1c) Nn )
4 addceq2 4384 . . . . . . . . 9 (y = (x +c 1c) → (A +c y) = (A +c (x +c 1c)))
54eqeq2d 2364 . . . . . . . 8 (y = (x +c 1c) → (B = (A +c y) ↔ B = (A +c (x +c 1c))))
65rspcev 2955 . . . . . . 7 (((x +c 1c) Nn B = (A +c (x +c 1c))) → y Nn B = (A +c y))
73, 6sylan 457 . . . . . 6 ((x Nn B = (A +c (x +c 1c))) → y Nn B = (A +c y))
82, 7sylan2b 461 . . . . 5 ((x Nn B = ((A +c x) +c 1c)) → y Nn B = (A +c y))
98rexlimiva 2733 . . . 4 (x Nn B = ((A +c x) +c 1c) → y Nn B = (A +c y))
109adantl 452 . . 3 ((A x Nn B = ((A +c x) +c 1c)) → y Nn B = (A +c y))
1110a1i 10 . 2 ((A V B W) → ((A x Nn B = ((A +c x) +c 1c)) → y Nn B = (A +c y)))
12 opkltfing 4449 . 2 ((A V B W) → (⟪A, B <fin ↔ (A x Nn B = ((A +c x) +c 1c))))
13 opklefing 4448 . 2 ((A V B W) → (⟪A, Bfiny Nn B = (A +c y)))
1411, 12, 133imtr4d 259 1 ((A V B W) → (⟪A, B <fin → ⟪A, Bfin ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 358   = wceq 1642   ∈ wcel 1710   ≠ wne 2516  ∃wrex 2615  ∅c0 3550  ⟪copk 4057  1cc1c 4134   Nn cnnc 4373   +c cplc 4375   ≤fin clefin 4432
 Copyright terms: Public domain W3C validator