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

Theorem ltfintri 4466
 Description: Trichotomy law for finite less than. (Contributed by SF, 29-Jan-2015.)
Assertion
Ref Expression
ltfintri ((M Nn N Nn M) → (⟪M, N <fin M = N N, M <fin ))

Proof of Theorem ltfintri
Dummy variables m n k p are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opkeq2 4060 . . . . . . . 8 (n = N → ⟪M, n⟫ = ⟪M, N⟫)
21eleq1d 2419 . . . . . . 7 (n = N → (⟪M, n <fin ↔ ⟪M, N <fin ))
3 eqeq2 2362 . . . . . . 7 (n = N → (M = nM = N))
4 opkeq1 4059 . . . . . . . 8 (n = N → ⟪n, M⟫ = ⟪N, M⟫)
54eleq1d 2419 . . . . . . 7 (n = N → (⟪n, M <fin ↔ ⟪N, M <fin ))
62, 3, 53orbi123d 1251 . . . . . 6 (n = N → ((⟪M, n <fin M = n n, M <fin ) ↔ (⟪M, N <fin M = N N, M <fin )))
76imbi2d 307 . . . . 5 (n = N → ((M → (⟪M, n <fin M = n n, M <fin )) ↔ (M → (⟪M, N <fin M = N N, M <fin ))))
87imbi2d 307 . . . 4 (n = N → ((M Nn → (M → (⟪M, n <fin M = n n, M <fin ))) ↔ (M Nn → (M → (⟪M, N <fin M = N N, M <fin )))))
9 ltfintrilem1 4465 . . . . . 6 {k (n Nn → (k → (⟪k, n <fin k = n n, k <fin )))} V
10 neeq1 2524 . . . . . . . 8 (k = 0c → (k ↔ 0c))
11 opkeq1 4059 . . . . . . . . . 10 (k = 0c → ⟪k, n⟫ = ⟪0c, n⟫)
1211eleq1d 2419 . . . . . . . . 9 (k = 0c → (⟪k, n <fin ↔ ⟪0c, n <fin ))
13 eqeq1 2359 . . . . . . . . 9 (k = 0c → (k = n ↔ 0c = n))
14 opkeq2 4060 . . . . . . . . . 10 (k = 0c → ⟪n, k⟫ = ⟪n, 0c⟫)
1514eleq1d 2419 . . . . . . . . 9 (k = 0c → (⟪n, k <fin ↔ ⟪n, 0c <fin ))
1612, 13, 153orbi123d 1251 . . . . . . . 8 (k = 0c → ((⟪k, n <fin k = n n, k <fin ) ↔ (⟪0c, n <fin 0c = n n, 0c <fin )))
1710, 16imbi12d 311 . . . . . . 7 (k = 0c → ((k → (⟪k, n <fin k = n n, k <fin )) ↔ (0c → (⟪0c, n <fin 0c = n n, 0c <fin ))))
1817imbi2d 307 . . . . . 6 (k = 0c → ((n Nn → (k → (⟪k, n <fin k = n n, k <fin ))) ↔ (n Nn → (0c → (⟪0c, n <fin 0c = n n, 0c <fin )))))
19 neeq1 2524 . . . . . . . 8 (k = m → (km))
20 opkeq1 4059 . . . . . . . . . 10 (k = m → ⟪k, n⟫ = ⟪m, n⟫)
2120eleq1d 2419 . . . . . . . . 9 (k = m → (⟪k, n <fin ↔ ⟪m, n <fin ))
22 eqeq1 2359 . . . . . . . . 9 (k = m → (k = nm = n))
23 opkeq2 4060 . . . . . . . . . 10 (k = m → ⟪n, k⟫ = ⟪n, m⟫)
2423eleq1d 2419 . . . . . . . . 9 (k = m → (⟪n, k <fin ↔ ⟪n, m <fin ))
2521, 22, 243orbi123d 1251 . . . . . . . 8 (k = m → ((⟪k, n <fin k = n n, k <fin ) ↔ (⟪m, n <fin m = n n, m <fin )))
2619, 25imbi12d 311 . . . . . . 7 (k = m → ((k → (⟪k, n <fin k = n n, k <fin )) ↔ (m → (⟪m, n <fin m = n n, m <fin ))))
2726imbi2d 307 . . . . . 6 (k = m → ((n Nn → (k → (⟪k, n <fin k = n n, k <fin ))) ↔ (n Nn → (m → (⟪m, n <fin m = n n, m <fin )))))
28 neeq1 2524 . . . . . . . 8 (k = (m +c 1c) → (k ↔ (m +c 1c) ≠ ))
29 opkeq1 4059 . . . . . . . . . 10 (k = (m +c 1c) → ⟪k, n⟫ = ⟪(m +c 1c), n⟫)
3029eleq1d 2419 . . . . . . . . 9 (k = (m +c 1c) → (⟪k, n <fin ↔ ⟪(m +c 1c), n <fin ))
31 eqeq1 2359 . . . . . . . . 9 (k = (m +c 1c) → (k = n ↔ (m +c 1c) = n))
32 opkeq2 4060 . . . . . . . . . 10 (k = (m +c 1c) → ⟪n, k⟫ = ⟪n, (m +c 1c)⟫)
3332eleq1d 2419 . . . . . . . . 9 (k = (m +c 1c) → (⟪n, k <fin ↔ ⟪n, (m +c 1c)⟫ <fin ))
3430, 31, 333orbi123d 1251 . . . . . . . 8 (k = (m +c 1c) → ((⟪k, n <fin k = n n, k <fin ) ↔ (⟪(m +c 1c), n <fin (m +c 1c) = n n, (m +c 1c)⟫ <fin )))
3528, 34imbi12d 311 . . . . . . 7 (k = (m +c 1c) → ((k → (⟪k, n <fin k = n n, k <fin )) ↔ ((m +c 1c) ≠ → (⟪(m +c 1c), n <fin (m +c 1c) = n n, (m +c 1c)⟫ <fin ))))
3635imbi2d 307 . . . . . 6 (k = (m +c 1c) → ((n Nn → (k → (⟪k, n <fin k = n n, k <fin ))) ↔ (n Nn → ((m +c 1c) ≠ → (⟪(m +c 1c), n <fin (m +c 1c) = n n, (m +c 1c)⟫ <fin )))))
37 neeq1 2524 . . . . . . . 8 (k = M → (kM))
38 opkeq1 4059 . . . . . . . . . 10 (k = M → ⟪k, n⟫ = ⟪M, n⟫)
3938eleq1d 2419 . . . . . . . . 9 (k = M → (⟪k, n <fin ↔ ⟪M, n <fin ))
40 eqeq1 2359 . . . . . . . . 9 (k = M → (k = nM = n))
41 opkeq2 4060 . . . . . . . . . 10 (k = M → ⟪n, k⟫ = ⟪n, M⟫)
4241eleq1d 2419 . . . . . . . . 9 (k = M → (⟪n, k <fin ↔ ⟪n, M <fin ))
4339, 40, 423orbi123d 1251 . . . . . . . 8 (k = M → ((⟪k, n <fin k = n n, k <fin ) ↔ (⟪M, n <fin M = n n, M <fin )))
4437, 43imbi12d 311 . . . . . . 7 (k = M → ((k → (⟪k, n <fin k = n n, k <fin )) ↔ (M → (⟪M, n <fin M = n n, M <fin ))))
4544imbi2d 307 . . . . . 6 (k = M → ((n Nn → (k → (⟪k, n <fin k = n n, k <fin ))) ↔ (n Nn → (M → (⟪M, n <fin M = n n, M <fin )))))
46 0cminle 4461 . . . . . . . . . 10 (n Nn → ⟪0c, nfin )
4746adantr 451 . . . . . . . . 9 ((n Nn 0c) → ⟪0c, nfin )
48 0cex 4392 . . . . . . . . . . 11 0c V
49 lefinlteq 4463 . . . . . . . . . . 11 ((0c V n Nn 0c) → (⟪0c, nfin ↔ (⟪0c, n <fin 0c = n)))
5048, 49mp3an1 1264 . . . . . . . . . 10 ((n Nn 0c) → (⟪0c, nfin ↔ (⟪0c, n <fin 0c = n)))
51 orcom 376 . . . . . . . . . 10 ((⟪0c, n <fin 0c = n) ↔ (0c = n ⟪0c, n <fin ))
5250, 51syl6bb 252 . . . . . . . . 9 ((n Nn 0c) → (⟪0c, nfin ↔ (0c = n ⟪0c, n <fin )))
5347, 52mpbid 201 . . . . . . . 8 ((n Nn 0c) → (0c = n ⟪0c, n <fin ))
54 3mix2 1125 . . . . . . . . 9 (0c = n → (⟪0c, n <fin 0c = n n, 0c <fin ))
55 3mix1 1124 . . . . . . . . 9 (⟪0c, n <fin → (⟪0c, n <fin 0c = n n, 0c <fin ))
5654, 55jaoi 368 . . . . . . . 8 ((0c = n ⟪0c, n <fin ) → (⟪0c, n <fin 0c = n n, 0c <fin ))
5753, 56syl 15 . . . . . . 7 ((n Nn 0c) → (⟪0c, n <fin 0c = n n, 0c <fin ))
5857ex 423 . . . . . 6 (n Nn → (0c → (⟪0c, n <fin 0c = n n, 0c <fin )))
59 addcnnul 4453 . . . . . . . . . . . . 13 ((m +c 1c) ≠ → (m 1c))
6059simpld 445 . . . . . . . . . . . 12 ((m +c 1c) ≠ m)
61603ad2ant3 978 . . . . . . . . . . 11 ((m Nn n Nn (m +c 1c) ≠ ) → m)
62 addc32 4416 . . . . . . . . . . . . . . . . . . . 20 ((m +c p) +c 1c) = ((m +c 1c) +c p)
6362eqeq2i 2363 . . . . . . . . . . . . . . . . . . 19 (n = ((m +c p) +c 1c) ↔ n = ((m +c 1c) +c p))
6463rexbii 2639 . . . . . . . . . . . . . . . . . 18 (p Nn n = ((m +c p) +c 1c) ↔ p Nn n = ((m +c 1c) +c p))
6564biimpi 186 . . . . . . . . . . . . . . . . 17 (p Nn n = ((m +c p) +c 1c) → p Nn n = ((m +c 1c) +c p))
6665adantl 452 . . . . . . . . . . . . . . . 16 ((m p Nn n = ((m +c p) +c 1c)) → p Nn n = ((m +c 1c) +c p))
6766a1i 10 . . . . . . . . . . . . . . 15 ((m Nn n Nn (m +c 1c) ≠ ) → ((m p Nn n = ((m +c p) +c 1c)) → p Nn n = ((m +c 1c) +c p)))
68 opkltfing 4449 . . . . . . . . . . . . . . . 16 ((m Nn n Nn ) → (⟪m, n <fin ↔ (m p Nn n = ((m +c p) +c 1c))))
69683adant3 975 . . . . . . . . . . . . . . 15 ((m Nn n Nn (m +c 1c) ≠ ) → (⟪m, n <fin ↔ (m p Nn n = ((m +c p) +c 1c))))
70 simp1 955 . . . . . . . . . . . . . . . . 17 ((m Nn n Nn (m +c 1c) ≠ ) → m Nn )
71 peano2 4403 . . . . . . . . . . . . . . . . 17 (m Nn → (m +c 1c) Nn )
7270, 71syl 15 . . . . . . . . . . . . . . . 16 ((m Nn n Nn (m +c 1c) ≠ ) → (m +c 1c) Nn )
73 simp2 956 . . . . . . . . . . . . . . . 16 ((m Nn n Nn (m +c 1c) ≠ ) → n Nn )
74 opklefing 4448 . . . . . . . . . . . . . . . 16 (((m +c 1c) Nn n Nn ) → (⟪(m +c 1c), nfinp Nn n = ((m +c 1c) +c p)))
7572, 73, 74syl2anc 642 . . . . . . . . . . . . . . 15 ((m Nn n Nn (m +c 1c) ≠ ) → (⟪(m +c 1c), nfinp Nn n = ((m +c 1c) +c p)))
7667, 69, 753imtr4d 259 . . . . . . . . . . . . . 14 ((m Nn n Nn (m +c 1c) ≠ ) → (⟪m, n <fin → ⟪(m +c 1c), nfin ))
77 lefinlteq 4463 . . . . . . . . . . . . . . 15 (((m +c 1c) Nn n Nn (m +c 1c) ≠ ) → (⟪(m +c 1c), nfin ↔ (⟪(m +c 1c), n <fin (m +c 1c) = n)))
7871, 77syl3an1 1215 . . . . . . . . . . . . . 14 ((m Nn n Nn (m +c 1c) ≠ ) → (⟪(m +c 1c), nfin ↔ (⟪(m +c 1c), n <fin (m +c 1c) = n)))
7976, 78sylibd 205 . . . . . . . . . . . . 13 ((m Nn n Nn (m +c 1c) ≠ ) → (⟪m, n <fin → (⟪(m +c 1c), n <fin (m +c 1c) = n)))
80 3mix1 1124 . . . . . . . . . . . . . 14 (⟪(m +c 1c), n <fin → (⟪(m +c 1c), n <fin (m +c 1c) = n n, (m +c 1c)⟫ <fin ))
81 3mix2 1125 . . . . . . . . . . . . . 14 ((m +c 1c) = n → (⟪(m +c 1c), n <fin (m +c 1c) = n n, (m +c 1c)⟫ <fin ))
8280, 81jaoi 368 . . . . . . . . . . . . 13 ((⟪(m +c 1c), n <fin (m +c 1c) = n) → (⟪(m +c 1c), n <fin (m +c 1c) = n n, (m +c 1c)⟫ <fin ))
8379, 82syl6 29 . . . . . . . . . . . 12 ((m Nn n Nn (m +c 1c) ≠ ) → (⟪m, n <fin → (⟪(m +c 1c), n <fin (m +c 1c) = n n, (m +c 1c)⟫ <fin )))
84 ltfinp1 4462 . . . . . . . . . . . . . . . 16 ((m Nn m) → ⟪m, (m +c 1c)⟫ <fin )
8560, 84sylan2 460 . . . . . . . . . . . . . . 15 ((m Nn (m +c 1c) ≠ ) → ⟪m, (m +c 1c)⟫ <fin )
86853adant2 974 . . . . . . . . . . . . . 14 ((m Nn n Nn (m +c 1c) ≠ ) → ⟪m, (m +c 1c)⟫ <fin )
87 opkeq1 4059 . . . . . . . . . . . . . . 15 (m = n → ⟪m, (m +c 1c)⟫ = ⟪n, (m +c 1c)⟫)
8887eleq1d 2419 . . . . . . . . . . . . . 14 (m = n → (⟪m, (m +c 1c)⟫ <fin ↔ ⟪n, (m +c 1c)⟫ <fin ))
8986, 88syl5ibcom 211 . . . . . . . . . . . . 13 ((m Nn n Nn (m +c 1c) ≠ ) → (m = n → ⟪n, (m +c 1c)⟫ <fin ))
90 3mix3 1126 . . . . . . . . . . . . 13 (⟪n, (m +c 1c)⟫ <fin → (⟪(m +c 1c), n <fin (m +c 1c) = n n, (m +c 1c)⟫ <fin ))
9189, 90syl6 29 . . . . . . . . . . . 12 ((m Nn n Nn (m +c 1c) ≠ ) → (m = n → (⟪(m +c 1c), n <fin (m +c 1c) = n n, (m +c 1c)⟫ <fin )))
92 ltfintr 4459 . . . . . . . . . . . . . . 15 ((n Nn m Nn (m +c 1c) Nn ) → ((⟪n, m <fin m, (m +c 1c)⟫ <fin ) → ⟪n, (m +c 1c)⟫ <fin ))
9373, 70, 72, 92syl3anc 1182 . . . . . . . . . . . . . 14 ((m Nn n Nn (m +c 1c) ≠ ) → ((⟪n, m <fin m, (m +c 1c)⟫ <fin ) → ⟪n, (m +c 1c)⟫ <fin ))
9486, 93mpan2d 655 . . . . . . . . . . . . 13 ((m Nn n Nn (m +c 1c) ≠ ) → (⟪n, m <fin → ⟪n, (m +c 1c)⟫ <fin ))
9594, 90syl6 29 . . . . . . . . . . . 12 ((m Nn n Nn (m +c 1c) ≠ ) → (⟪n, m <fin → (⟪(m +c 1c), n <fin (m +c 1c) = n n, (m +c 1c)⟫ <fin )))
9683, 91, 953jaod 1246 . . . . . . . . . . 11 ((m Nn n Nn (m +c 1c) ≠ ) → ((⟪m, n <fin m = n n, m <fin ) → (⟪(m +c 1c), n <fin (m +c 1c) = n n, (m +c 1c)⟫ <fin )))
9761, 96embantd 50 . . . . . . . . . 10 ((m Nn n Nn (m +c 1c) ≠ ) → ((m → (⟪m, n <fin m = n n, m <fin )) → (⟪(m +c 1c), n <fin (m +c 1c) = n n, (m +c 1c)⟫ <fin )))
98973expia 1153 . . . . . . . . 9 ((m Nn n Nn ) → ((m +c 1c) ≠ → ((m → (⟪m, n <fin m = n n, m <fin )) → (⟪(m +c 1c), n <fin (m +c 1c) = n n, (m +c 1c)⟫ <fin ))))
9998com23 72 . . . . . . . 8 ((m Nn n Nn ) → ((m → (⟪m, n <fin m = n n, m <fin )) → ((m +c 1c) ≠ → (⟪(m +c 1c), n <fin (m +c 1c) = n n, (m +c 1c)⟫ <fin ))))
10099ex 423 . . . . . . 7 (m Nn → (n Nn → ((m → (⟪m, n <fin m = n n, m <fin )) → ((m +c 1c) ≠ → (⟪(m +c 1c), n <fin (m +c 1c) = n n, (m +c 1c)⟫ <fin )))))
101100a2d 23 . . . . . 6 (m Nn → ((n Nn → (m → (⟪m, n <fin m = n n, m <fin ))) → (n Nn → ((m +c 1c) ≠ → (⟪(m +c 1c), n <fin (m +c 1c) = n n, (m +c 1c)⟫ <fin )))))
1029, 18, 27, 36, 45, 58, 101finds 4411 . . . . 5 (M Nn → (n Nn → (M → (⟪M, n <fin M = n n, M <fin ))))
103102com12 27 . . . 4 (n Nn → (M Nn → (M → (⟪M, n <fin M = n n, M <fin ))))
1048, 103vtoclga 2920 . . 3 (N Nn → (M Nn → (M → (⟪M, N <fin M = N N, M <fin ))))
105104com12 27 . 2 (M Nn → (N Nn → (M → (⟪M, N <fin M = N N, M <fin ))))
1061053imp 1145 1 ((M Nn N Nn M) → (⟪M, N <fin M = N N, M <fin ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∨ wo 357   ∧ wa 358   ∨ w3o 933   ∧ w3a 934   = wceq 1642   ∈ wcel 1710   ≠ wne 2516  ∃wrex 2615  Vcvv 2859  ∅c0 3550  ⟪copk 4057  1cc1c 4134   Nn cnnc 4373  0cc0c 4374   +c cplc 4375   ≤fin clefin 4432
 Copyright terms: Public domain W3C validator