NFE Home 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   <fin cltfin 4433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-0c 4377  df-addc 4378  df-nnc 4379  df-lefin 4440  df-ltfin 4441
This theorem is referenced by:  lenltfin  4469  tfinltfin  4501  sfin111  4536
  Copyright terms: Public domain W3C validator