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

Theorem ltfinirr 4457
 Description: Irreflexive law for finite less than. (Contributed by SF, 29-Jan-2015.)
Assertion
Ref Expression
ltfinirr (A Nn → ¬ ⟪A, A <fin )

Proof of Theorem ltfinirr
Dummy variable x is distinct from all other variables.
StepHypRef Expression
1 0cnsuc 4401 . . . . . . . 8 (x +c 1c) ≠ 0c
21necomi 2598 . . . . . . 7 0c ≠ (x +c 1c)
3 df-ne 2518 . . . . . . 7 (0c ≠ (x +c 1c) ↔ ¬ 0c = (x +c 1c))
42, 3mpbi 199 . . . . . 6 ¬ 0c = (x +c 1c)
5 addcid1 4405 . . . . . . . . 9 (A +c 0c) = A
65eqcomi 2357 . . . . . . . 8 A = (A +c 0c)
7 addcass 4415 . . . . . . . 8 ((A +c x) +c 1c) = (A +c (x +c 1c))
86, 7eqeq12i 2366 . . . . . . 7 (A = ((A +c x) +c 1c) ↔ (A +c 0c) = (A +c (x +c 1c)))
9 simpll 730 . . . . . . . 8 (((A Nn A) x Nn ) → A Nn )
10 peano1 4402 . . . . . . . . 9 0c Nn
1110a1i 10 . . . . . . . 8 (((A Nn A) x Nn ) → 0c Nn )
12 peano2 4403 . . . . . . . . 9 (x Nn → (x +c 1c) Nn )
1312adantl 452 . . . . . . . 8 (((A Nn A) x Nn ) → (x +c 1c) Nn )
145neeq1i 2526 . . . . . . . . . 10 ((A +c 0c) ≠ A)
1514biimpri 197 . . . . . . . . 9 (A → (A +c 0c) ≠ )
1615ad2antlr 707 . . . . . . . 8 (((A Nn A) x Nn ) → (A +c 0c) ≠ )
17 preaddccan2 4455 . . . . . . . 8 (((A Nn 0c Nn (x +c 1c) Nn ) (A +c 0c) ≠ ) → ((A +c 0c) = (A +c (x +c 1c)) ↔ 0c = (x +c 1c)))
189, 11, 13, 16, 17syl31anc 1185 . . . . . . 7 (((A Nn A) x Nn ) → ((A +c 0c) = (A +c (x +c 1c)) ↔ 0c = (x +c 1c)))
198, 18syl5bb 248 . . . . . 6 (((A Nn A) x Nn ) → (A = ((A +c x) +c 1c) ↔ 0c = (x +c 1c)))
204, 19mtbiri 294 . . . . 5 (((A Nn A) x Nn ) → ¬ A = ((A +c x) +c 1c))
2120nrexdv 2717 . . . 4 ((A Nn A) → ¬ x Nn A = ((A +c x) +c 1c))
2221ex 423 . . 3 (A Nn → (A → ¬ x Nn A = ((A +c x) +c 1c)))
23 imnan 411 . . 3 ((A → ¬ x Nn A = ((A +c x) +c 1c)) ↔ ¬ (A x Nn A = ((A +c x) +c 1c)))
2422, 23sylib 188 . 2 (A Nn → ¬ (A x Nn A = ((A +c x) +c 1c)))
25 opkltfing 4449 . . 3 ((A Nn A Nn ) → (⟪A, A <fin ↔ (A x Nn A = ((A +c x) +c 1c))))
2625anidms 626 . 2 (A Nn → (⟪A, A <fin ↔ (A x Nn A = ((A +c x) +c 1c))))
2724, 26mtbird 292 1 (A Nn → ¬ ⟪A, A <fin )
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358   = wceq 1642   ∈ wcel 1710   ≠ wne 2516  ∃wrex 2615  ∅c0 3550  ⟪copk 4057  1cc1c 4134   Nn cnnc 4373  0cc0c 4374   +c cplc 4375
 Copyright terms: Public domain W3C validator