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

Theorem tfinltfinlem1 4500
 Description: Lemma for tfinltfin 4501. Prove the forward direction of the theorem. (Contributed by SF, 2-Feb-2015.)
Assertion
Ref Expression
tfinltfinlem1 ((M Nn N Nn ) → (⟪M, N <fin → ⟪ Tfin M, Tfin N <fin ))

Proof of Theorem tfinltfinlem1
Dummy variables x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tfinnnul 4490 . . . . . 6 ((M Nn M) → Tfin M)
21ex 423 . . . . 5 (M Nn → (MTfin M))
32adantrd 454 . . . 4 (M Nn → ((M x Nn N = ((M +c x) +c 1c)) → Tfin M))
43adantr 451 . . 3 ((M Nn N Nn ) → ((M x Nn N = ((M +c x) +c 1c)) → Tfin M))
5 addcnul1 4452 . . . . . . . . . . . . . 14 (1c +c ) =
6 addccom 4406 . . . . . . . . . . . . . 14 (1c +c ) = ( +c 1c)
75, 6eqtr3i 2375 . . . . . . . . . . . . 13 = ( +c 1c)
8 addceq2 4384 . . . . . . . . . . . . . . . . 17 (y = → ( Tfin M +c y) = ( Tfin M +c ))
9 addcnul1 4452 . . . . . . . . . . . . . . . . 17 ( Tfin M +c ) =
108, 9syl6eq 2401 . . . . . . . . . . . . . . . 16 (y = → ( Tfin M +c y) = )
1110addceq1d 4389 . . . . . . . . . . . . . . 15 (y = → (( Tfin M +c y) +c 1c) = ( +c 1c))
1211eqeq2d 2364 . . . . . . . . . . . . . 14 (y = → ( = (( Tfin M +c y) +c 1c) ↔ = ( +c 1c)))
1312rspcev 2955 . . . . . . . . . . . . 13 (( Nn = ( +c 1c)) → y Nn = (( Tfin M +c y) +c 1c))
147, 13mpan2 652 . . . . . . . . . . . 12 ( Nny Nn = (( Tfin M +c y) +c 1c))
15 eleq1 2413 . . . . . . . . . . . . 13 (N = → (N Nn Nn ))
16 tfineq 4488 . . . . . . . . . . . . . . . 16 (N = Tfin N = Tfin )
17 tfinnul 4491 . . . . . . . . . . . . . . . 16 Tfin =
1816, 17syl6eq 2401 . . . . . . . . . . . . . . 15 (N = Tfin N = )
1918eqeq1d 2361 . . . . . . . . . . . . . 14 (N = → ( Tfin N = (( Tfin M +c y) +c 1c) ↔ = (( Tfin M +c y) +c 1c)))
2019rexbidv 2635 . . . . . . . . . . . . 13 (N = → (y Nn Tfin N = (( Tfin M +c y) +c 1c) ↔ y Nn = (( Tfin M +c y) +c 1c)))
2115, 20imbi12d 311 . . . . . . . . . . . 12 (N = → ((N Nny Nn Tfin N = (( Tfin M +c y) +c 1c)) ↔ ( Nny Nn = (( Tfin M +c y) +c 1c))))
2214, 21mpbiri 224 . . . . . . . . . . 11 (N = → (N Nny Nn Tfin N = (( Tfin M +c y) +c 1c)))
2322adantld 453 . . . . . . . . . 10 (N = → ((M Nn N Nn ) → y Nn Tfin N = (( Tfin M +c y) +c 1c)))
2423adantrd 454 . . . . . . . . 9 (N = → (((M Nn N Nn ) (M x Nn )) → y Nn Tfin N = (( Tfin M +c y) +c 1c)))
2524a1dd 42 . . . . . . . 8 (N = → (((M Nn N Nn ) (M x Nn )) → (N = ((M +c x) +c 1c) → y Nn Tfin N = (( Tfin M +c y) +c 1c))))
26 simp2r 982 . . . . . . . . . . . . 13 (((M Nn N Nn ) (M x Nn ) (N N = ((M +c x) +c 1c))) → x Nn )
27 simp3r 984 . . . . . . . . . . . . . . . . . 18 (((M Nn N Nn ) (M x Nn ) (N N = ((M +c x) +c 1c))) → N = ((M +c x) +c 1c))
28 simp3l 983 . . . . . . . . . . . . . . . . . 18 (((M Nn N Nn ) (M x Nn ) (N N = ((M +c x) +c 1c))) → N)
2927, 28eqnetrrd 2536 . . . . . . . . . . . . . . . . 17 (((M Nn N Nn ) (M x Nn ) (N N = ((M +c x) +c 1c))) → ((M +c x) +c 1c) ≠ )
30 addcnnul 4453 . . . . . . . . . . . . . . . . 17 (((M +c x) +c 1c) ≠ → ((M +c x) ≠ 1c))
3129, 30syl 15 . . . . . . . . . . . . . . . 16 (((M Nn N Nn ) (M x Nn ) (N N = ((M +c x) +c 1c))) → ((M +c x) ≠ 1c))
3231simpld 445 . . . . . . . . . . . . . . 15 (((M Nn N Nn ) (M x Nn ) (N N = ((M +c x) +c 1c))) → (M +c x) ≠ )
33 addcnnul 4453 . . . . . . . . . . . . . . 15 ((M +c x) ≠ → (M x))
3432, 33syl 15 . . . . . . . . . . . . . 14 (((M Nn N Nn ) (M x Nn ) (N N = ((M +c x) +c 1c))) → (M x))
3534simprd 449 . . . . . . . . . . . . 13 (((M Nn N Nn ) (M x Nn ) (N N = ((M +c x) +c 1c))) → x)
36 tfinprop 4489 . . . . . . . . . . . . . 14 ((x Nn x) → ( Tfin x Nn y x 1y Tfin x))
3736simpld 445 . . . . . . . . . . . . 13 ((x Nn x) → Tfin x Nn )
3826, 35, 37syl2anc 642 . . . . . . . . . . . 12 (((M Nn N Nn ) (M x Nn ) (N N = ((M +c x) +c 1c))) → Tfin x Nn )
39 tfineq 4488 . . . . . . . . . . . . . . . 16 (N = ((M +c x) +c 1c) → Tfin N = Tfin ((M +c x) +c 1c))
4039adantl 452 . . . . . . . . . . . . . . 15 ((N N = ((M +c x) +c 1c)) → Tfin N = Tfin ((M +c x) +c 1c))
41403ad2ant3 978 . . . . . . . . . . . . . 14 (((M Nn N Nn ) (M x Nn ) (N N = ((M +c x) +c 1c))) → Tfin N = Tfin ((M +c x) +c 1c))
42 simp1l 979 . . . . . . . . . . . . . . . 16 (((M Nn N Nn ) (M x Nn ) (N N = ((M +c x) +c 1c))) → M Nn )
43 nncaddccl 4419 . . . . . . . . . . . . . . . 16 ((M Nn x Nn ) → (M +c x) Nn )
4442, 26, 43syl2anc 642 . . . . . . . . . . . . . . 15 (((M Nn N Nn ) (M x Nn ) (N N = ((M +c x) +c 1c))) → (M +c x) Nn )
45 tfinsuc 4498 . . . . . . . . . . . . . . 15 (((M +c x) Nn ((M +c x) +c 1c) ≠ ) → Tfin ((M +c x) +c 1c) = ( Tfin (M +c x) +c 1c))
4644, 29, 45syl2anc 642 . . . . . . . . . . . . . 14 (((M Nn N Nn ) (M x Nn ) (N N = ((M +c x) +c 1c))) → Tfin ((M +c x) +c 1c) = ( Tfin (M +c x) +c 1c))
4741, 46eqtrd 2385 . . . . . . . . . . . . 13 (((M Nn N Nn ) (M x Nn ) (N N = ((M +c x) +c 1c))) → Tfin N = ( Tfin (M +c x) +c 1c))
48 tfindi 4496 . . . . . . . . . . . . . . 15 ((M Nn x Nn (M +c x) ≠ ) → Tfin (M +c x) = ( Tfin M +c Tfin x))
4942, 26, 32, 48syl3anc 1182 . . . . . . . . . . . . . 14 (((M Nn N Nn ) (M x Nn ) (N N = ((M +c x) +c 1c))) → Tfin (M +c x) = ( Tfin M +c Tfin x))
5049addceq1d 4389 . . . . . . . . . . . . 13 (((M Nn N Nn ) (M x Nn ) (N N = ((M +c x) +c 1c))) → ( Tfin (M +c x) +c 1c) = (( Tfin M +c Tfin x) +c 1c))
5147, 50eqtrd 2385 . . . . . . . . . . . 12 (((M Nn N Nn ) (M x Nn ) (N N = ((M +c x) +c 1c))) → Tfin N = (( Tfin M +c Tfin x) +c 1c))
52 addceq2 4384 . . . . . . . . . . . . . . 15 (y = Tfin x → ( Tfin M +c y) = ( Tfin M +c Tfin x))
5352addceq1d 4389 . . . . . . . . . . . . . 14 (y = Tfin x → (( Tfin M +c y) +c 1c) = (( Tfin M +c Tfin x) +c 1c))
5453eqeq2d 2364 . . . . . . . . . . . . 13 (y = Tfin x → ( Tfin N = (( Tfin M +c y) +c 1c) ↔ Tfin N = (( Tfin M +c Tfin x) +c 1c)))
5554rspcev 2955 . . . . . . . . . . . 12 (( Tfin x Nn Tfin N = (( Tfin M +c Tfin x) +c 1c)) → y Nn Tfin N = (( Tfin M +c y) +c 1c))
5638, 51, 55syl2anc 642 . . . . . . . . . . 11 (((M Nn N Nn ) (M x Nn ) (N N = ((M +c x) +c 1c))) → y Nn Tfin N = (( Tfin M +c y) +c 1c))
57563expa 1151 . . . . . . . . . 10 ((((M Nn N Nn ) (M x Nn )) (N N = ((M +c x) +c 1c))) → y Nn Tfin N = (( Tfin M +c y) +c 1c))
5857exp32 588 . . . . . . . . 9 (((M Nn N Nn ) (M x Nn )) → (N → (N = ((M +c x) +c 1c) → y Nn Tfin N = (( Tfin M +c y) +c 1c))))
5958com12 27 . . . . . . . 8 (N → (((M Nn N Nn ) (M x Nn )) → (N = ((M +c x) +c 1c) → y Nn Tfin N = (( Tfin M +c y) +c 1c))))
6025, 59pm2.61ine 2592 . . . . . . 7 (((M Nn N Nn ) (M x Nn )) → (N = ((M +c x) +c 1c) → y Nn Tfin N = (( Tfin M +c y) +c 1c)))
6160expr 598 . . . . . 6 (((M Nn N Nn ) M) → (x Nn → (N = ((M +c x) +c 1c) → y Nn Tfin N = (( Tfin M +c y) +c 1c))))
6261rexlimdv 2737 . . . . 5 (((M Nn N Nn ) M) → (x Nn N = ((M +c x) +c 1c) → y Nn Tfin N = (( Tfin M +c y) +c 1c)))
6362ex 423 . . . 4 ((M Nn N Nn ) → (M → (x Nn N = ((M +c x) +c 1c) → y Nn Tfin N = (( Tfin M +c y) +c 1c))))
6463imp3a 420 . . 3 ((M Nn N Nn ) → ((M x Nn N = ((M +c x) +c 1c)) → y Nn Tfin N = (( Tfin M +c y) +c 1c)))
654, 64jcad 519 . 2 ((M Nn N Nn ) → ((M x Nn N = ((M +c x) +c 1c)) → ( Tfin M y Nn Tfin N = (( Tfin M +c y) +c 1c))))
66 opkltfing 4449 . 2 ((M Nn N Nn ) → (⟪M, N <fin ↔ (M x Nn N = ((M +c x) +c 1c))))
67 tfinex 4485 . . . 4 Tfin M V
68 tfinex 4485 . . . 4 Tfin N V
69 opkltfing 4449 . . . 4 (( Tfin M V Tfin N V) → (⟪ Tfin M, Tfin N <fin ↔ ( Tfin M y Nn Tfin N = (( Tfin M +c y) +c 1c))))
7067, 68, 69mp2an 653 . . 3 (⟪ Tfin M, Tfin N <fin ↔ ( Tfin M y Nn Tfin N = (( Tfin M +c y) +c 1c)))
7170a1i 10 . 2 ((M Nn N Nn ) → (⟪ Tfin M, Tfin N <fin ↔ ( Tfin M y Nn Tfin N = (( Tfin M +c y) +c 1c))))
7265, 66, 713imtr4d 259 1 ((M Nn N Nn ) → (⟪M, N <fin → ⟪ Tfin M, Tfin N <fin ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358   ∧ 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