Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cantnfcl Structured version   Unicode version

Theorem cantnfcl 8103
 Description: Basic properties of the order isomorphism used later. The support of an is a finite subset of , so it is well-ordered by and the order isomorphism has domain a finite ordinal. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 28-Jun-2019.)
Hypotheses
Ref Expression
cantnfs.s CNF
cantnfs.a
cantnfs.b
cantnfcl.g OrdIso supp
cantnfcl.f
Assertion
Ref Expression
cantnfcl supp

Proof of Theorem cantnfcl
StepHypRef Expression
1 suppssdm 6930 . . . . 5 supp
2 cantnfcl.f . . . . . . . 8
3 cantnfs.s . . . . . . . . 9 CNF
4 cantnfs.a . . . . . . . . 9
5 cantnfs.b . . . . . . . . 9
63, 4, 5cantnfs 8102 . . . . . . . 8 finSupp
72, 6mpbid 210 . . . . . . 7 finSupp
87simpld 459 . . . . . 6
9 fdm 5741 . . . . . 6
108, 9syl 16 . . . . 5
111, 10syl5sseq 3547 . . . 4 supp
12 onss 6625 . . . . 5
135, 12syl 16 . . . 4
1411, 13sstrd 3509 . . 3 supp
15 epweon 6618 . . 3
16 wess 4875 . . 3 supp supp
1714, 15, 16mpisyl 18 . 2 supp
18 ovex 6324 . . . . . 6 supp
1918a1i 11 . . . . 5 supp
20 cantnfcl.g . . . . . 6 OrdIso supp
2120oion 7979 . . . . 5 supp
2219, 21syl 16 . . . 4
237simprd 463 . . . . . 6 finSupp
2423fsuppimpd 7854 . . . . 5 supp
2520oien 7981 . . . . . 6 supp supp supp
2619, 17, 25syl2anc 661 . . . . 5 supp
27 enfii 7756 . . . . 5 supp supp
2824, 26, 27syl2anc 661 . . . 4
2922, 28elind 3684 . . 3
30 onfin2 7728 . . 3
3129, 30syl6eleqr 2556 . 2
3217, 31jca 532 1 supp
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   wceq 1395   wcel 1819  cvv 3109   cin 3470   wss 3471  c0 3793   class class class wbr 4456   cep 4798   wwe 4846  con0 4887   cdm 5008  wf 5590  (class class class)co 6296  com 6699   supp csupp 6917   cen 7532  cfn 7535   finSupp cfsupp 7847  OrdIsocoi 7952   CNF ccnf 8095 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-fal 1401  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-iun 4334  df-br 4457  df-opab 4516  df-mpt 4517  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-se 4848  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6700  df-supp 6918  df-recs 7060  df-rdg 7094  df-seqom 7131  df-er 7329  df-map 7440  df-en 7536  df-dom 7537  df-sdom 7538  df-fin 7539  df-fsupp 7848  df-oi 7953  df-cnf 8096 This theorem is referenced by:  cantnfval2  8105  cantnfle  8107  cantnflt  8108  cantnflt2  8109  cantnff  8110  cantnfp1lem2  8115  cantnfp1lem3  8116  cantnflem1b  8122  cantnflem1d  8124  cantnflem1  8125  cnfcomlem  8160  cnfcom  8161  cnfcom2lem  8162  cnfcom3lem  8164
 Copyright terms: Public domain W3C validator