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

Theorem tfinlefin 4502
 Description: Ordering rule for the finite T operation. Theorem X.1.33 of [Rosser] p. 529. (Contributed by SF, 2-Feb-2015.)
Assertion
Ref Expression
tfinlefin ((M Nn N Nn ) → (⟪M, Nfin ↔ ⟪ Tfin M, Tfin Nfin ))

Proof of Theorem tfinlefin
StepHypRef Expression
1 tfinltfin 4501 . . . 4 ((N Nn M Nn ) → (⟪N, M <fin ↔ ⟪ Tfin N, Tfin M <fin ))
21ancoms 439 . . 3 ((M Nn N Nn ) → (⟪N, M <fin ↔ ⟪ Tfin N, Tfin M <fin ))
32notbid 285 . 2 ((M Nn N Nn ) → (¬ ⟪N, M <fin ↔ ¬ ⟪ Tfin N, Tfin M <fin ))
4 lenltfin 4469 . 2 ((M Nn N Nn ) → (⟪M, Nfin ↔ ¬ ⟪N, M <fin ))
5 tfincl 4492 . . 3 (M NnTfin M Nn )
6 tfincl 4492 . . 3 (N NnTfin N Nn )
7 lenltfin 4469 . . 3 (( Tfin M Nn Tfin N Nn ) → (⟪ Tfin M, Tfin Nfin ↔ ¬ ⟪ Tfin N, Tfin M <fin ))
85, 6, 7syl2an 463 . 2 ((M Nn N Nn ) → (⟪ Tfin M, Tfin Nfin ↔ ¬ ⟪ Tfin N, Tfin M <fin ))
93, 4, 83bitr4d 276 1 ((M Nn N Nn ) → (⟪M, Nfin ↔ ⟪ Tfin M, Tfin Nfin ))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358   ∈ wcel 1710  ⟪copk 4057   Nn cnnc 4373   ≤fin clefin 4432
 Copyright terms: Public domain W3C validator