![]() |
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 5363. (Revised by BTernaryTau, 10-Jan-2025.) |
Ref | Expression |
---|---|
xpfi | ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unfi 9169 | . . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin) | |
2 | pwfi 9175 | . . . 4 ⊢ ((𝐴 ∪ 𝐵) ∈ Fin ↔ 𝒫 (𝐴 ∪ 𝐵) ∈ Fin) | |
3 | pwfi 9175 | . . . 4 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ Fin ↔ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin) | |
4 | 2, 3 | bitri 275 | . . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ Fin ↔ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin) |
5 | 1, 4 | sylib 217 | . 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin) |
6 | xpsspw 5808 | . 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) | |
7 | ssfi 9170 | . 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 3946 ⊆ wss 3948 𝒫 cpw 4602 × cxp 5674 Fincfn 8936 |
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 5299 ax-nul 5306 ax-pr 5427 ax-un 7722 |
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 3778 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-om 7853 df-1o 8463 df-en 8937 df-fin 8940 |
This theorem is referenced by: 3xpfi 9316 mapfi 9345 fsuppxpfi 9377 infxpenlem 10005 ficardadju 10191 ackbij1lem9 10220 ackbij1lem10 10221 hashxplem 14390 hashmap 14392 fsum2dlem 15713 fsumcom2 15717 ackbijnn 15771 fprod2dlem 15921 fprodcom2 15925 rexpen 16168 crth 16708 phimullem 16709 prmreclem3 16848 gsumcom3fi 19842 ablfaclem3 19952 gsumdixp 20125 frlmbas3 21323 gsumbagdiagOLD 21484 psrass1lemOLD 21485 gsumbagdiag 21487 psrass1lem 21488 evlslem2 21634 mamudm 21882 mamufacex 21883 mamures 21884 mamucl 21893 mamudi 21895 mamudir 21896 mamuvs1 21897 mamuvs2 21898 matsca2 21914 matbas2 21915 matplusg2 21921 matvsca2 21922 matplusgcell 21927 matsubgcell 21928 matvscacell 21930 matgsum 21931 mamumat1cl 21933 mattposcl 21947 mdetrsca 22097 mdetunilem9 22114 pmatcoe1fsupp 22195 tsmsxplem1 23649 tsmsxplem2 23650 tsmsxp 23651 i1fadd 25204 i1fmul 25205 itg1addlem4 25208 itg1addlem4OLD 25209 fsumdvdsmul 26689 fsumvma 26706 lgsquadlem1 26873 lgsquadlem2 26874 lgsquadlem3 26875 relfi 31821 fsumiunle 32023 matdim 32689 fedgmullem1 32703 sibfof 33328 hgt750lemb 33657 erdszelem10 34180 matunitlindflem2 36474 matunitlindf 36475 poimirlem26 36503 poimirlem27 36504 poimirlem28 36505 cntotbnd 36653 sticksstones22 40973 pellex 41559 mnringmulrcld 42973 fourierdlem42 44852 etransclem44 44981 etransclem45 44982 etransclem47 44984 |
Copyright terms: Public domain | W3C validator |