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

Theorem leconnnc 6218
Description: Cardinal less than or equal is total over the naturals. (Contributed by SF, 12-Mar-2015.)
Assertion
Ref Expression
leconnnc ((A Nn B Nn ) → (Ac B Bc A))

Proof of Theorem leconnnc
Dummy variables a m n p are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq2 4643 . . . . . 6 (n = B → (Ac nAc B))
2 breq1 4642 . . . . . 6 (n = B → (nc ABc A))
31, 2orbi12d 690 . . . . 5 (n = B → ((Ac n nc A) ↔ (Ac B Bc A)))
43imbi2d 307 . . . 4 (n = B → ((A Nn → (Ac n nc A)) ↔ (A Nn → (Ac B Bc A))))
5 elun 3220 . . . . . . . . . . . 12 (a ((c “ {n}) ∪ ( ≤c “ {n})) ↔ (a (c “ {n}) a ( ≤c “ {n})))
6 eliniseg 5020 . . . . . . . . . . . . 13 (a (c “ {n}) ↔ ac n)
7 elimasn 5019 . . . . . . . . . . . . . 14 (a ( ≤c “ {n}) ↔ n, a c )
8 df-br 4640 . . . . . . . . . . . . . 14 (nc an, a c )
97, 8bitr4i 243 . . . . . . . . . . . . 13 (a ( ≤c “ {n}) ↔ nc a)
106, 9orbi12i 507 . . . . . . . . . . . 12 ((a (c “ {n}) a ( ≤c “ {n})) ↔ (ac n nc a))
115, 10bitri 240 . . . . . . . . . . 11 (a ((c “ {n}) ∪ ( ≤c “ {n})) ↔ (ac n nc a))
1211abbi2i 2464 . . . . . . . . . 10 ((c “ {n}) ∪ ( ≤c “ {n})) = {a (ac n nc a)}
1312uneq2i 3415 . . . . . . . . 9 ({a ¬ n Nn } ∪ ((c “ {n}) ∪ ( ≤c “ {n}))) = ({a ¬ n Nn } ∪ {a (ac n nc a)})
14 unab 3521 . . . . . . . . 9 ({a ¬ n Nn } ∪ {a (ac n nc a)}) = {a n Nn (ac n nc a))}
1513, 14eqtri 2373 . . . . . . . 8 ({a ¬ n Nn } ∪ ((c “ {n}) ∪ ( ≤c “ {n}))) = {a n Nn (ac n nc a))}
16 imor 401 . . . . . . . . 9 ((n Nn → (ac n nc a)) ↔ (¬ n Nn (ac n nc a)))
1716abbii 2465 . . . . . . . 8 {a (n Nn → (ac n nc a))} = {a n Nn (ac n nc a))}
1815, 17eqtr4i 2376 . . . . . . 7 ({a ¬ n Nn } ∪ ((c “ {n}) ∪ ( ≤c “ {n}))) = {a (n Nn → (ac n nc a))}
19 abexv 4324 . . . . . . . 8 {a ¬ n Nn } V
20 lecex 6115 . . . . . . . . . . 11 c V
2120cnvex 5102 . . . . . . . . . 10 c V
22 snex 4111 . . . . . . . . . 10 {n} V
2321, 22imaex 4747 . . . . . . . . 9 (c “ {n}) V
2420, 22imaex 4747 . . . . . . . . 9 ( ≤c “ {n}) V
2523, 24unex 4106 . . . . . . . 8 ((c “ {n}) ∪ ( ≤c “ {n})) V
2619, 25unex 4106 . . . . . . 7 ({a ¬ n Nn } ∪ ((c “ {n}) ∪ ( ≤c “ {n}))) V
2718, 26eqeltrri 2424 . . . . . 6 {a (n Nn → (ac n nc a))} V
28 breq1 4642 . . . . . . . 8 (a = 0c → (ac n ↔ 0cc n))
29 breq2 4643 . . . . . . . 8 (a = 0c → (nc anc 0c))
3028, 29orbi12d 690 . . . . . . 7 (a = 0c → ((ac n nc a) ↔ (0cc n nc 0c)))
3130imbi2d 307 . . . . . 6 (a = 0c → ((n Nn → (ac n nc a)) ↔ (n Nn → (0cc n nc 0c))))
32 breq1 4642 . . . . . . . 8 (a = m → (ac nmc n))
33 breq2 4643 . . . . . . . 8 (a = m → (nc anc m))
3432, 33orbi12d 690 . . . . . . 7 (a = m → ((ac n nc a) ↔ (mc n nc m)))
3534imbi2d 307 . . . . . 6 (a = m → ((n Nn → (ac n nc a)) ↔ (n Nn → (mc n nc m))))
36 breq1 4642 . . . . . . . 8 (a = (m +c 1c) → (ac n ↔ (m +c 1c) ≤c n))
37 breq2 4643 . . . . . . . 8 (a = (m +c 1c) → (nc anc (m +c 1c)))
3836, 37orbi12d 690 . . . . . . 7 (a = (m +c 1c) → ((ac n nc a) ↔ ((m +c 1c) ≤c n nc (m +c 1c))))
3938imbi2d 307 . . . . . 6 (a = (m +c 1c) → ((n Nn → (ac n nc a)) ↔ (n Nn → ((m +c 1c) ≤c n nc (m +c 1c)))))
40 breq1 4642 . . . . . . . 8 (a = A → (ac nAc n))
41 breq2 4643 . . . . . . . 8 (a = A → (nc anc A))
4240, 41orbi12d 690 . . . . . . 7 (a = A → ((ac n nc a) ↔ (Ac n nc A)))
4342imbi2d 307 . . . . . 6 (a = A → ((n Nn → (ac n nc a)) ↔ (n Nn → (Ac n nc A))))
44 nnnc 6146 . . . . . . . 8 (n Nnn NC )
45 le0nc 6200 . . . . . . . 8 (n NC → 0cc n)
4644, 45syl 15 . . . . . . 7 (n Nn → 0cc n)
47 orc 374 . . . . . . 7 (0cc n → (0cc n nc 0c))
4846, 47syl 15 . . . . . 6 (n Nn → (0cc n nc 0c))
49 nnnc 6146 . . . . . . . . 9 (m Nnm NC )
50 dflec2 6210 . . . . . . . . . . 11 ((m NC n NC ) → (mc np NC n = (m +c p)))
51 nc0le1 6216 . . . . . . . . . . . . . . . . . 18 (p NC → (p = 0c 1cc p))
52 1cnc 6139 . . . . . . . . . . . . . . . . . . . . . 22 1c NC
53 le0nc 6200 . . . . . . . . . . . . . . . . . . . . . 22 (1c NC → 0cc 1c)
5452, 53ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 0cc 1c
55 breq1 4642 . . . . . . . . . . . . . . . . . . . . 21 (p = 0c → (pc 1c ↔ 0cc 1c))
5654, 55mpbiri 224 . . . . . . . . . . . . . . . . . . . 20 (p = 0cpc 1c)
5756orim1i 503 . . . . . . . . . . . . . . . . . . 19 ((p = 0c 1cc p) → (pc 1c 1cc p))
5857a1i 10 . . . . . . . . . . . . . . . . . 18 (p NC → ((p = 0c 1cc p) → (pc 1c 1cc p)))
5951, 58mpd 14 . . . . . . . . . . . . . . . . 17 (p NC → (pc 1c 1cc p))
6059orcomd 377 . . . . . . . . . . . . . . . 16 (p NC → (1cc p pc 1c))
6160adantl 452 . . . . . . . . . . . . . . 15 ((m NC p NC ) → (1cc p pc 1c))
62 simpll 730 . . . . . . . . . . . . . . . . . 18 (((m NC p NC ) 1cc p) → m NC )
6352a1i 10 . . . . . . . . . . . . . . . . . 18 (((m NC p NC ) 1cc p) → 1c NC )
64 simplr 731 . . . . . . . . . . . . . . . . . 18 (((m NC p NC ) 1cc p) → p NC )
65 simpr 447 . . . . . . . . . . . . . . . . . 18 (((m NC p NC ) 1cc p) → 1cc p)
66 leaddc2 6215 . . . . . . . . . . . . . . . . . 18 (((m NC 1c NC p NC ) 1cc p) → (m +c 1c) ≤c (m +c p))
6762, 63, 64, 65, 66syl31anc 1185 . . . . . . . . . . . . . . . . 17 (((m NC p NC ) 1cc p) → (m +c 1c) ≤c (m +c p))
6867ex 423 . . . . . . . . . . . . . . . 16 ((m NC p NC ) → (1cc p → (m +c 1c) ≤c (m +c p)))
69 simpll 730 . . . . . . . . . . . . . . . . . 18 (((m NC p NC ) pc 1c) → m NC )
70 simplr 731 . . . . . . . . . . . . . . . . . 18 (((m NC p NC ) pc 1c) → p NC )
7152a1i 10 . . . . . . . . . . . . . . . . . 18 (((m NC p NC ) pc 1c) → 1c NC )
72 simpr 447 . . . . . . . . . . . . . . . . . 18 (((m NC p NC ) pc 1c) → pc 1c)
73 leaddc2 6215 . . . . . . . . . . . . . . . . . 18 (((m NC p NC 1c NC ) pc 1c) → (m +c p) ≤c (m +c 1c))
7469, 70, 71, 72, 73syl31anc 1185 . . . . . . . . . . . . . . . . 17 (((m NC p NC ) pc 1c) → (m +c p) ≤c (m +c 1c))
7574ex 423 . . . . . . . . . . . . . . . 16 ((m NC p NC ) → (pc 1c → (m +c p) ≤c (m +c 1c)))
7668, 75orim12d 811 . . . . . . . . . . . . . . 15 ((m NC p NC ) → ((1cc p pc 1c) → ((m +c 1c) ≤c (m +c p) (m +c p) ≤c (m +c 1c))))
7761, 76mpd 14 . . . . . . . . . . . . . 14 ((m NC p NC ) → ((m +c 1c) ≤c (m +c p) (m +c p) ≤c (m +c 1c)))
78 breq2 4643 . . . . . . . . . . . . . . . . 17 (n = (m +c p) → ((m +c 1c) ≤c n ↔ (m +c 1c) ≤c (m +c p)))
79 breq1 4642 . . . . . . . . . . . . . . . . 17 (n = (m +c p) → (nc (m +c 1c) ↔ (m +c p) ≤c (m +c 1c)))
8078, 79orbi12d 690 . . . . . . . . . . . . . . . 16 (n = (m +c p) → (((m +c 1c) ≤c n nc (m +c 1c)) ↔ ((m +c 1c) ≤c (m +c p) (m +c p) ≤c (m +c 1c))))
8180biimprd 214 . . . . . . . . . . . . . . 15 (n = (m +c p) → (((m +c 1c) ≤c (m +c p) (m +c p) ≤c (m +c 1c)) → ((m +c 1c) ≤c n nc (m +c 1c))))
8281com12 27 . . . . . . . . . . . . . 14 (((m +c 1c) ≤c (m +c p) (m +c p) ≤c (m +c 1c)) → (n = (m +c p) → ((m +c 1c) ≤c n nc (m +c 1c))))
8377, 82syl 15 . . . . . . . . . . . . 13 ((m NC p NC ) → (n = (m +c p) → ((m +c 1c) ≤c n nc (m +c 1c))))
8483rexlimdva 2738 . . . . . . . . . . . 12 (m NC → (p NC n = (m +c p) → ((m +c 1c) ≤c n nc (m +c 1c))))
8584adantr 451 . . . . . . . . . . 11 ((m NC n NC ) → (p NC n = (m +c p) → ((m +c 1c) ≤c n nc (m +c 1c))))
8650, 85sylbid 206 . . . . . . . . . 10 ((m NC n NC ) → (mc n → ((m +c 1c) ≤c n nc (m +c 1c))))
87 addlecncs 6209 . . . . . . . . . . . . . . 15 ((m NC 1c NC ) → mc (m +c 1c))
8852, 87mpan2 652 . . . . . . . . . . . . . 14 (m NCmc (m +c 1c))
8988adantl 452 . . . . . . . . . . . . 13 ((n NC m NC ) → mc (m +c 1c))
90 peano2nc 6145 . . . . . . . . . . . . . . 15 (m NC → (m +c 1c) NC )
9190adantl 452 . . . . . . . . . . . . . 14 ((n NC m NC ) → (m +c 1c) NC )
92 lectr 6211 . . . . . . . . . . . . . 14 ((n NC m NC (m +c 1c) NC ) → ((nc m mc (m +c 1c)) → nc (m +c 1c)))
9391, 92mpd3an3 1278 . . . . . . . . . . . . 13 ((n NC m NC ) → ((nc m mc (m +c 1c)) → nc (m +c 1c)))
9489, 93mpan2d 655 . . . . . . . . . . . 12 ((n NC m NC ) → (nc mnc (m +c 1c)))
9594ancoms 439 . . . . . . . . . . 11 ((m NC n NC ) → (nc mnc (m +c 1c)))
96 olc 373 . . . . . . . . . . 11 (nc (m +c 1c) → ((m +c 1c) ≤c n nc (m +c 1c)))
9795, 96syl6 29 . . . . . . . . . 10 ((m NC n NC ) → (nc m → ((m +c 1c) ≤c n nc (m +c 1c))))
9886, 97jaod 369 . . . . . . . . 9 ((m NC n NC ) → ((mc n nc m) → ((m +c 1c) ≤c n nc (m +c 1c))))
9949, 44, 98syl2an 463 . . . . . . . 8 ((m Nn n Nn ) → ((mc n nc m) → ((m +c 1c) ≤c n nc (m +c 1c))))
10099ex 423 . . . . . . 7 (m Nn → (n Nn → ((mc n nc m) → ((m +c 1c) ≤c n nc (m +c 1c)))))
101100a2d 23 . . . . . 6 (m Nn → ((n Nn → (mc n nc m)) → (n Nn → ((m +c 1c) ≤c n nc (m +c 1c)))))
10227, 31, 35, 39, 43, 48, 101finds 4411 . . . . 5 (A Nn → (n Nn → (Ac n nc A)))
103102com12 27 . . . 4 (n Nn → (A Nn → (Ac n nc A)))
1044, 103vtoclga 2920 . . 3 (B Nn → (A Nn → (Ac B Bc A)))
105104com12 27 . 2 (A Nn → (B Nn → (Ac B Bc A)))
106105imp 418 1 ((A Nn B Nn ) → (Ac B Bc A))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   wo 357   wa 358   = wceq 1642   wcel 1710  {cab 2339  wrex 2615  Vcvv 2859  cun 3207  {csn 3737  1cc1c 4134   Nn cnnc 4373  0cc0c 4374   +c cplc 4375  cop 4561   class class class wbr 4639  cima 4722  ccnv 4771   NC cncs 6088  c clec 6089
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-13 1712  ax-14 1714  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-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  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-pss 3261  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-idk 4195  df-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380  df-lefin 4440  df-ltfin 4441  df-ncfin 4442  df-tfin 4443  df-evenfin 4444  df-oddfin 4445  df-sfin 4446  df-spfin 4447  df-phi 4565  df-op 4566  df-proj1 4567  df-proj2 4568  df-opab 4623  df-br 4640  df-1st 4723  df-swap 4724  df-sset 4725  df-co 4726  df-ima 4727  df-si 4728  df-id 4767  df-xp 4784  df-cnv 4785  df-rn 4786  df-dm 4787  df-res 4788  df-fun 4789  df-fn 4790  df-f 4791  df-f1 4792  df-fo 4793  df-f1o 4794  df-fv 4795  df-2nd 4797  df-txp 5736  df-ins2 5750  df-ins3 5752  df-image 5754  df-ins4 5756  df-si3 5758  df-funs 5760  df-fns 5762  df-trans 5899  df-sym 5908  df-er 5909  df-ec 5947  df-qs 5951  df-en 6029  df-ncs 6098  df-lec 6099  df-nc 6101
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator