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

Theorem tfinltfin 4501
 Description: Ordering rule for the finite T operation. Corollary to theorem X.1.33 of [Rosser] p. 529. (Contributed by SF, 1-Feb-2015.)
Assertion
Ref Expression
tfinltfin ((M Nn N Nn ) → (⟪M, N <fin ↔ ⟪ Tfin M, Tfin N <fin ))

Proof of Theorem tfinltfin
Dummy variables x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tfinltfinlem1 4500 . 2 ((M Nn N Nn ) → (⟪M, N <fin → ⟪ Tfin M, Tfin N <fin ))
2 tfineq 4488 . . . . . . . . 9 (M = Tfin M = Tfin )
3 tfinnul 4491 . . . . . . . . 9 Tfin =
42, 3syl6eq 2401 . . . . . . . 8 (M = Tfin M = )
5 df-ne 2518 . . . . . . . . 9 ( Tfin M ↔ ¬ Tfin M = )
65con2bii 322 . . . . . . . 8 ( Tfin M = ↔ ¬ Tfin M)
74, 6sylib 188 . . . . . . 7 (M = → ¬ Tfin M)
87intnanrd 883 . . . . . 6 (M = → ¬ ( Tfin M x Nn Tfin N = (( Tfin M +c x) +c 1c)))
9 tfinex 4485 . . . . . . 7 Tfin M V
10 tfinex 4485 . . . . . . 7 Tfin N V
11 opkltfing 4449 . . . . . . 7 (( Tfin M V Tfin N V) → (⟪ Tfin M, Tfin N <fin ↔ ( Tfin M x Nn Tfin N = (( Tfin M +c x) +c 1c))))
129, 10, 11mp2an 653 . . . . . 6 (⟪ Tfin M, Tfin N <fin ↔ ( Tfin M x Nn Tfin N = (( Tfin M +c x) +c 1c)))
138, 12sylnibr 296 . . . . 5 (M = → ¬ ⟪ Tfin M, Tfin N <fin )
1413pm2.21d 98 . . . 4 (M = → (⟪ Tfin M, Tfin N <fin → ⟪M, N <fin ))
1514a1d 22 . . 3 (M = → ((M Nn N Nn ) → (⟪ Tfin M, Tfin N <fin → ⟪M, N <fin )))
16 tfinprop 4489 . . . . . . . . . . . . . 14 ((M Nn M) → ( Tfin M Nn y M 1y Tfin M))
1716simpld 445 . . . . . . . . . . . . 13 ((M Nn M) → Tfin M Nn )
18 ltfinirr 4457 . . . . . . . . . . . . 13 ( Tfin M Nn → ¬ ⟪ Tfin M, Tfin M <fin )
1917, 18syl 15 . . . . . . . . . . . 12 ((M Nn M) → ¬ ⟪ Tfin M, Tfin M <fin )
20193adant2 974 . . . . . . . . . . 11 ((M Nn N Nn M) → ¬ ⟪ Tfin M, Tfin M <fin )
21 opkeq2 4060 . . . . . . . . . . . . 13 ( Tfin M = Tfin N → ⟪ Tfin M, Tfin M⟫ = ⟪ Tfin M, Tfin N⟫)
2221eleq1d 2419 . . . . . . . . . . . 12 ( Tfin M = Tfin N → (⟪ Tfin M, Tfin M <fin ↔ ⟪ Tfin M, Tfin N <fin ))
2322notbid 285 . . . . . . . . . . 11 ( Tfin M = Tfin N → (¬ ⟪ Tfin M, Tfin M <fin ↔ ¬ ⟪ Tfin M, Tfin N <fin ))
2420, 23syl5ibcom 211 . . . . . . . . . 10 ((M Nn N Nn M) → ( Tfin M = Tfin N → ¬ ⟪ Tfin M, Tfin N <fin ))
2524con2d 107 . . . . . . . . 9 ((M Nn N Nn M) → (⟪ Tfin M, Tfin N <fin → ¬ Tfin M = Tfin N))
2625imp 418 . . . . . . . 8 (((M Nn N Nn M) Tfin M, Tfin N <fin ) → ¬ Tfin M = Tfin N)
27 tfineq 4488 . . . . . . . 8 (M = NTfin M = Tfin N)
2826, 27nsyl 113 . . . . . . 7 (((M Nn N Nn M) Tfin M, Tfin N <fin ) → ¬ M = N)
29 simpl1 958 . . . . . . . . . . . . 13 (((M Nn N Nn M) (⟪ Tfin M, Tfin N <fin N)) → M Nn )
30 simpl3 960 . . . . . . . . . . . . 13 (((M Nn N Nn M) (⟪ Tfin M, Tfin N <fin N)) → M)
3129, 30, 17syl2anc 642 . . . . . . . . . . . 12 (((M Nn N Nn M) (⟪ Tfin M, Tfin N <fin N)) → Tfin M Nn )
32 simpl2 959 . . . . . . . . . . . . 13 (((M Nn N Nn M) (⟪ Tfin M, Tfin N <fin N)) → N Nn )
33 simprr 733 . . . . . . . . . . . . 13 (((M Nn N Nn M) (⟪ Tfin M, Tfin N <fin N)) → N)
34 tfinprop 4489 . . . . . . . . . . . . . 14 ((N Nn N) → ( Tfin N Nn y N 1y Tfin N))
3534simpld 445 . . . . . . . . . . . . 13 ((N Nn N) → Tfin N Nn )
3632, 33, 35syl2anc 642 . . . . . . . . . . . 12 (((M Nn N Nn M) (⟪ Tfin M, Tfin N <fin N)) → Tfin N Nn )
3731, 36jca 518 . . . . . . . . . . 11 (((M Nn N Nn M) (⟪ Tfin M, Tfin N <fin N)) → ( Tfin M Nn Tfin N Nn ))
38 simprl 732 . . . . . . . . . . 11 (((M Nn N Nn M) (⟪ Tfin M, Tfin N <fin N)) → ⟪ Tfin M, Tfin N <fin )
39 ltfinasym 4460 . . . . . . . . . . 11 (( Tfin M Nn Tfin N Nn ) → (⟪ Tfin M, Tfin N <fin → ¬ ⟪ Tfin N, Tfin M <fin ))
4037, 38, 39sylc 56 . . . . . . . . . 10 (((M Nn N Nn M) (⟪ Tfin M, Tfin N <fin N)) → ¬ ⟪ Tfin N, Tfin M <fin )
4140expr 598 . . . . . . . . 9 (((M Nn N Nn M) Tfin M, Tfin N <fin ) → (N → ¬ ⟪ Tfin N, Tfin M <fin ))
42 imnan 411 . . . . . . . . 9 ((N → ¬ ⟪ Tfin N, Tfin M <fin ) ↔ ¬ (N Tfin N, Tfin M <fin ))
4341, 42sylib 188 . . . . . . . 8 (((M Nn N Nn M) Tfin M, Tfin N <fin ) → ¬ (N Tfin N, Tfin M <fin ))
44 opkltfing 4449 . . . . . . . . . . . . . 14 ((N Nn M Nn ) → (⟪N, M <fin ↔ (N y Nn M = ((N +c y) +c 1c))))
4544ancoms 439 . . . . . . . . . . . . 13 ((M Nn N Nn ) → (⟪N, M <fin ↔ (N y Nn M = ((N +c y) +c 1c))))
46453adant3 975 . . . . . . . . . . . 12 ((M Nn N Nn M) → (⟪N, M <fin ↔ (N y Nn M = ((N +c y) +c 1c))))
4746simprbda 606 . . . . . . . . . . 11 (((M Nn N Nn M) N, M <fin ) → N)
4847adantrl 696 . . . . . . . . . 10 (((M Nn N Nn M) (⟪ Tfin M, Tfin N <fin N, M <fin )) → N)
49 simpl2 959 . . . . . . . . . . . 12 (((M Nn N Nn M) (⟪ Tfin M, Tfin N <fin N, M <fin )) → N Nn )
50 simpl1 958 . . . . . . . . . . . 12 (((M Nn N Nn M) (⟪ Tfin M, Tfin N <fin N, M <fin )) → M Nn )
5149, 50jca 518 . . . . . . . . . . 11 (((M Nn N Nn M) (⟪ Tfin M, Tfin N <fin N, M <fin )) → (N Nn M Nn ))
52 simprr 733 . . . . . . . . . . 11 (((M Nn N Nn M) (⟪ Tfin M, Tfin N <fin N, M <fin )) → ⟪N, M <fin )
53 tfinltfinlem1 4500 . . . . . . . . . . 11 ((N Nn M Nn ) → (⟪N, M <fin → ⟪ Tfin N, Tfin M <fin ))
5451, 52, 53sylc 56 . . . . . . . . . 10 (((M Nn N Nn M) (⟪ Tfin M, Tfin N <fin N, M <fin )) → ⟪ Tfin N, Tfin M <fin )
5548, 54jca 518 . . . . . . . . 9 (((M Nn N Nn M) (⟪ Tfin M, Tfin N <fin N, M <fin )) → (N Tfin N, Tfin M <fin ))
5655expr 598 . . . . . . . 8 (((M Nn N Nn M) Tfin M, Tfin N <fin ) → (⟪N, M <fin → (N Tfin N, Tfin M <fin )))
5743, 56mtod 168 . . . . . . 7 (((M Nn N Nn M) Tfin M, Tfin N <fin ) → ¬ ⟪N, M <fin )
58 ltfintri 4466 . . . . . . . 8 ((M Nn N Nn M) → (⟪M, N <fin M = N N, M <fin ))
5958adantr 451 . . . . . . 7 (((M Nn N Nn M) Tfin M, Tfin N <fin ) → (⟪M, N <fin M = N N, M <fin ))
6028, 57, 59ecase23d 1285 . . . . . 6 (((M Nn N Nn M) Tfin M, Tfin N <fin ) → ⟪M, N <fin )
6160ex 423 . . . . 5 ((M Nn N Nn M) → (⟪ Tfin M, Tfin N <fin → ⟪M, N <fin ))
62613expa 1151 . . . 4 (((M Nn N Nn ) M) → (⟪ Tfin M, Tfin N <fin → ⟪M, N <fin ))
6362expcom 424 . . 3 (M → ((M Nn N Nn ) → (⟪ Tfin M, Tfin N <fin → ⟪M, N <fin )))
6415, 63pm2.61ine 2592 . 2 ((M Nn N Nn ) → (⟪ Tfin M, Tfin N <fin → ⟪M, N <fin ))
651, 64impbid 183 1 ((M Nn N Nn ) → (⟪M, N <fin ↔ ⟪ Tfin M, Tfin N <fin ))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358   ∨ w3o 933   ∧ w3a 934   = wceq 1642   ∈ wcel 1710   ≠ wne 2516  ∃wrex 2615  Vcvv 2859  ∅c0 3550  ⟪copk 4057  1cc1c 4134  ℘1cpw1 4135   Nn cnnc 4373   +c cplc 4375
 Copyright terms: Public domain W3C validator