![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > xpfi | Structured version Visualization version GIF version |
Description: The Cartesian product of two finite sets is finite. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Mar-2015.) Avoid ax-pow 5364. (Revised by BTernaryTau, 10-Jan-2025.) |
Ref | Expression |
---|---|
xpfi | ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unfi 9172 | . . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin) | |
2 | pwfi 9178 | . . . 4 ⊢ ((𝐴 ∪ 𝐵) ∈ Fin ↔ 𝒫 (𝐴 ∪ 𝐵) ∈ Fin) | |
3 | pwfi 9178 | . . . 4 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ Fin ↔ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin) | |
4 | 2, 3 | bitri 275 | . . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ Fin ↔ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin) |
5 | 1, 4 | sylib 217 | . 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin) |
6 | xpsspw 5810 | . 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) | |
7 | ssfi 9173 | . 2 ⊢ ((𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin ∧ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)) → (𝐴 × 𝐵) ∈ Fin) | |
8 | 5, 6, 7 | sylancl 587 | 1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∈ wcel 2107 ∪ cun 3947 ⊆ wss 3949 𝒫 cpw 4603 × cxp 5675 Fincfn 8939 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5428 ax-un 7725 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-ral 3063 df-rex 3072 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-om 7856 df-1o 8466 df-en 8940 df-fin 8943 |
This theorem is referenced by: 3xpfi 9319 mapfi 9348 fsuppxpfi 9380 infxpenlem 10008 ficardadju 10194 ackbij1lem9 10223 ackbij1lem10 10224 hashxplem 14393 hashmap 14395 fsum2dlem 15716 fsumcom2 15720 ackbijnn 15774 fprod2dlem 15924 fprodcom2 15928 rexpen 16171 crth 16711 phimullem 16712 prmreclem3 16851 gsumcom3fi 19847 ablfaclem3 19957 gsumdixp 20131 frlmbas3 21331 gsumbagdiagOLD 21492 psrass1lemOLD 21493 gsumbagdiag 21495 psrass1lem 21496 evlslem2 21642 mamudm 21890 mamufacex 21891 mamures 21892 mamucl 21901 mamudi 21903 mamudir 21904 mamuvs1 21905 mamuvs2 21906 matsca2 21922 matbas2 21923 matplusg2 21929 matvsca2 21930 matplusgcell 21935 matsubgcell 21936 matvscacell 21938 matgsum 21939 mamumat1cl 21941 mattposcl 21955 mdetrsca 22105 mdetunilem9 22122 pmatcoe1fsupp 22203 tsmsxplem1 23657 tsmsxplem2 23658 tsmsxp 23659 i1fadd 25212 i1fmul 25213 itg1addlem4 25216 itg1addlem4OLD 25217 fsumdvdsmul 26699 fsumvma 26716 lgsquadlem1 26883 lgsquadlem2 26884 lgsquadlem3 26885 relfi 31833 fsumiunle 32035 matdim 32700 fedgmullem1 32714 sibfof 33339 hgt750lemb 33668 erdszelem10 34191 matunitlindflem2 36485 matunitlindf 36486 poimirlem26 36514 poimirlem27 36515 poimirlem28 36516 cntotbnd 36664 sticksstones22 40984 pellex 41573 mnringmulrcld 42987 fourierdlem42 44865 etransclem44 44994 etransclem45 44995 etransclem47 44997 |
Copyright terms: Public domain | W3C validator |