Metamath Proof Explorer

Theorem xpfi

Description: The Cartesian product of two finite sets is finite. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 12-Mar-2015)

Ref Expression
Assertion xpfi ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to {A}×{B}\in \mathrm{Fin}$

Proof

Step Hyp Ref Expression
1 xpeq1 ${⊢}{x}=\varnothing \to {x}×{B}=\varnothing ×{B}$
2 1 eleq1d ${⊢}{x}=\varnothing \to \left({x}×{B}\in \mathrm{Fin}↔\varnothing ×{B}\in \mathrm{Fin}\right)$
3 2 imbi2d ${⊢}{x}=\varnothing \to \left(\left({B}\in \mathrm{Fin}\to {x}×{B}\in \mathrm{Fin}\right)↔\left({B}\in \mathrm{Fin}\to \varnothing ×{B}\in \mathrm{Fin}\right)\right)$
4 xpeq1 ${⊢}{x}={y}\setminus \left\{{z}\right\}\to {x}×{B}=\left({y}\setminus \left\{{z}\right\}\right)×{B}$
5 4 eleq1d ${⊢}{x}={y}\setminus \left\{{z}\right\}\to \left({x}×{B}\in \mathrm{Fin}↔\left({y}\setminus \left\{{z}\right\}\right)×{B}\in \mathrm{Fin}\right)$
6 5 imbi2d ${⊢}{x}={y}\setminus \left\{{z}\right\}\to \left(\left({B}\in \mathrm{Fin}\to {x}×{B}\in \mathrm{Fin}\right)↔\left({B}\in \mathrm{Fin}\to \left({y}\setminus \left\{{z}\right\}\right)×{B}\in \mathrm{Fin}\right)\right)$
7 xpeq1 ${⊢}{x}={y}\to {x}×{B}={y}×{B}$
8 7 eleq1d ${⊢}{x}={y}\to \left({x}×{B}\in \mathrm{Fin}↔{y}×{B}\in \mathrm{Fin}\right)$
9 8 imbi2d ${⊢}{x}={y}\to \left(\left({B}\in \mathrm{Fin}\to {x}×{B}\in \mathrm{Fin}\right)↔\left({B}\in \mathrm{Fin}\to {y}×{B}\in \mathrm{Fin}\right)\right)$
10 xpeq1 ${⊢}{x}={A}\to {x}×{B}={A}×{B}$
11 10 eleq1d ${⊢}{x}={A}\to \left({x}×{B}\in \mathrm{Fin}↔{A}×{B}\in \mathrm{Fin}\right)$
12 11 imbi2d ${⊢}{x}={A}\to \left(\left({B}\in \mathrm{Fin}\to {x}×{B}\in \mathrm{Fin}\right)↔\left({B}\in \mathrm{Fin}\to {A}×{B}\in \mathrm{Fin}\right)\right)$
13 0xp ${⊢}\varnothing ×{B}=\varnothing$
14 0fin ${⊢}\varnothing \in \mathrm{Fin}$
15 13 14 eqeltri ${⊢}\varnothing ×{B}\in \mathrm{Fin}$
16 15 a1i ${⊢}{B}\in \mathrm{Fin}\to \varnothing ×{B}\in \mathrm{Fin}$
17 neq0 ${⊢}¬{y}=\varnothing ↔\exists {w}\phantom{\rule{.4em}{0ex}}{w}\in {y}$
18 sneq ${⊢}{z}={w}\to \left\{{z}\right\}=\left\{{w}\right\}$
19 18 difeq2d ${⊢}{z}={w}\to {y}\setminus \left\{{z}\right\}={y}\setminus \left\{{w}\right\}$
20 19 xpeq1d ${⊢}{z}={w}\to \left({y}\setminus \left\{{z}\right\}\right)×{B}=\left({y}\setminus \left\{{w}\right\}\right)×{B}$
21 20 eleq1d ${⊢}{z}={w}\to \left(\left({y}\setminus \left\{{z}\right\}\right)×{B}\in \mathrm{Fin}↔\left({y}\setminus \left\{{w}\right\}\right)×{B}\in \mathrm{Fin}\right)$
22 21 imbi2d ${⊢}{z}={w}\to \left(\left({B}\in \mathrm{Fin}\to \left({y}\setminus \left\{{z}\right\}\right)×{B}\in \mathrm{Fin}\right)↔\left({B}\in \mathrm{Fin}\to \left({y}\setminus \left\{{w}\right\}\right)×{B}\in \mathrm{Fin}\right)\right)$
23 22 rspcv ${⊢}{w}\in {y}\to \left(\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\left({B}\in \mathrm{Fin}\to \left({y}\setminus \left\{{z}\right\}\right)×{B}\in \mathrm{Fin}\right)\to \left({B}\in \mathrm{Fin}\to \left({y}\setminus \left\{{w}\right\}\right)×{B}\in \mathrm{Fin}\right)\right)$
24 23 adantl ${⊢}\left(\left({y}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\wedge {w}\in {y}\right)\to \left(\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\left({B}\in \mathrm{Fin}\to \left({y}\setminus \left\{{z}\right\}\right)×{B}\in \mathrm{Fin}\right)\to \left({B}\in \mathrm{Fin}\to \left({y}\setminus \left\{{w}\right\}\right)×{B}\in \mathrm{Fin}\right)\right)$
25 pm2.27 ${⊢}{B}\in \mathrm{Fin}\to \left(\left({B}\in \mathrm{Fin}\to \left({y}\setminus \left\{{w}\right\}\right)×{B}\in \mathrm{Fin}\right)\to \left({y}\setminus \left\{{w}\right\}\right)×{B}\in \mathrm{Fin}\right)$
26 25 ad2antlr ${⊢}\left(\left({y}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\wedge {w}\in {y}\right)\to \left(\left({B}\in \mathrm{Fin}\to \left({y}\setminus \left\{{w}\right\}\right)×{B}\in \mathrm{Fin}\right)\to \left({y}\setminus \left\{{w}\right\}\right)×{B}\in \mathrm{Fin}\right)$
27 snex ${⊢}\left\{{w}\right\}\in \mathrm{V}$
28 xpexg ${⊢}\left(\left\{{w}\right\}\in \mathrm{V}\wedge {B}\in \mathrm{Fin}\right)\to \left\{{w}\right\}×{B}\in \mathrm{V}$
29 27 28 mpan ${⊢}{B}\in \mathrm{Fin}\to \left\{{w}\right\}×{B}\in \mathrm{V}$
30 id ${⊢}{B}\in \mathrm{Fin}\to {B}\in \mathrm{Fin}$
31 vex ${⊢}{w}\in \mathrm{V}$
32 2ndconst ${⊢}{w}\in \mathrm{V}\to \left({{2}^{nd}↾}_{\left(\left\{{w}\right\}×{B}\right)}\right):\left\{{w}\right\}×{B}\underset{1-1 onto}{⟶}{B}$
33 31 32 mp1i ${⊢}{B}\in \mathrm{Fin}\to \left({{2}^{nd}↾}_{\left(\left\{{w}\right\}×{B}\right)}\right):\left\{{w}\right\}×{B}\underset{1-1 onto}{⟶}{B}$
34 f1oen2g ${⊢}\left(\left\{{w}\right\}×{B}\in \mathrm{V}\wedge {B}\in \mathrm{Fin}\wedge \left({{2}^{nd}↾}_{\left(\left\{{w}\right\}×{B}\right)}\right):\left\{{w}\right\}×{B}\underset{1-1 onto}{⟶}{B}\right)\to \left(\left\{{w}\right\}×{B}\right)\approx {B}$
35 29 30 33 34 syl3anc ${⊢}{B}\in \mathrm{Fin}\to \left(\left\{{w}\right\}×{B}\right)\approx {B}$
36 enfii ${⊢}\left({B}\in \mathrm{Fin}\wedge \left(\left\{{w}\right\}×{B}\right)\approx {B}\right)\to \left\{{w}\right\}×{B}\in \mathrm{Fin}$
37 35 36 mpdan ${⊢}{B}\in \mathrm{Fin}\to \left\{{w}\right\}×{B}\in \mathrm{Fin}$
38 37 ad2antlr ${⊢}\left(\left({y}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\wedge {w}\in {y}\right)\to \left\{{w}\right\}×{B}\in \mathrm{Fin}$
39 unfi ${⊢}\left(\left({y}\setminus \left\{{w}\right\}\right)×{B}\in \mathrm{Fin}\wedge \left\{{w}\right\}×{B}\in \mathrm{Fin}\right)\to \left(\left({y}\setminus \left\{{w}\right\}\right)×{B}\right)\cup \left(\left\{{w}\right\}×{B}\right)\in \mathrm{Fin}$
40 xpundir ${⊢}\left(\left({y}\setminus \left\{{w}\right\}\right)\cup \left\{{w}\right\}\right)×{B}=\left(\left({y}\setminus \left\{{w}\right\}\right)×{B}\right)\cup \left(\left\{{w}\right\}×{B}\right)$
41 difsnid ${⊢}{w}\in {y}\to \left({y}\setminus \left\{{w}\right\}\right)\cup \left\{{w}\right\}={y}$
42 41 xpeq1d ${⊢}{w}\in {y}\to \left(\left({y}\setminus \left\{{w}\right\}\right)\cup \left\{{w}\right\}\right)×{B}={y}×{B}$
43 40 42 syl5eqr ${⊢}{w}\in {y}\to \left(\left({y}\setminus \left\{{w}\right\}\right)×{B}\right)\cup \left(\left\{{w}\right\}×{B}\right)={y}×{B}$
44 43 eleq1d ${⊢}{w}\in {y}\to \left(\left(\left({y}\setminus \left\{{w}\right\}\right)×{B}\right)\cup \left(\left\{{w}\right\}×{B}\right)\in \mathrm{Fin}↔{y}×{B}\in \mathrm{Fin}\right)$
45 44 biimpd ${⊢}{w}\in {y}\to \left(\left(\left({y}\setminus \left\{{w}\right\}\right)×{B}\right)\cup \left(\left\{{w}\right\}×{B}\right)\in \mathrm{Fin}\to {y}×{B}\in \mathrm{Fin}\right)$
46 45 adantl ${⊢}\left(\left({y}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\wedge {w}\in {y}\right)\to \left(\left(\left({y}\setminus \left\{{w}\right\}\right)×{B}\right)\cup \left(\left\{{w}\right\}×{B}\right)\in \mathrm{Fin}\to {y}×{B}\in \mathrm{Fin}\right)$
47 39 46 syl5 ${⊢}\left(\left({y}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\wedge {w}\in {y}\right)\to \left(\left(\left({y}\setminus \left\{{w}\right\}\right)×{B}\in \mathrm{Fin}\wedge \left\{{w}\right\}×{B}\in \mathrm{Fin}\right)\to {y}×{B}\in \mathrm{Fin}\right)$
48 38 47 mpan2d ${⊢}\left(\left({y}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\wedge {w}\in {y}\right)\to \left(\left({y}\setminus \left\{{w}\right\}\right)×{B}\in \mathrm{Fin}\to {y}×{B}\in \mathrm{Fin}\right)$
49 24 26 48 3syld ${⊢}\left(\left({y}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\wedge {w}\in {y}\right)\to \left(\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\left({B}\in \mathrm{Fin}\to \left({y}\setminus \left\{{z}\right\}\right)×{B}\in \mathrm{Fin}\right)\to {y}×{B}\in \mathrm{Fin}\right)$
50 49 ex ${⊢}\left({y}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to \left({w}\in {y}\to \left(\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\left({B}\in \mathrm{Fin}\to \left({y}\setminus \left\{{z}\right\}\right)×{B}\in \mathrm{Fin}\right)\to {y}×{B}\in \mathrm{Fin}\right)\right)$
51 50 exlimdv ${⊢}\left({y}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to \left(\exists {w}\phantom{\rule{.4em}{0ex}}{w}\in {y}\to \left(\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\left({B}\in \mathrm{Fin}\to \left({y}\setminus \left\{{z}\right\}\right)×{B}\in \mathrm{Fin}\right)\to {y}×{B}\in \mathrm{Fin}\right)\right)$
52 17 51 syl5bi ${⊢}\left({y}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to \left(¬{y}=\varnothing \to \left(\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\left({B}\in \mathrm{Fin}\to \left({y}\setminus \left\{{z}\right\}\right)×{B}\in \mathrm{Fin}\right)\to {y}×{B}\in \mathrm{Fin}\right)\right)$
53 xpeq1 ${⊢}{y}=\varnothing \to {y}×{B}=\varnothing ×{B}$
54 53 15 syl6eqel ${⊢}{y}=\varnothing \to {y}×{B}\in \mathrm{Fin}$
55 54 a1d ${⊢}{y}=\varnothing \to \left(\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\left({B}\in \mathrm{Fin}\to \left({y}\setminus \left\{{z}\right\}\right)×{B}\in \mathrm{Fin}\right)\to {y}×{B}\in \mathrm{Fin}\right)$
56 52 55 pm2.61d2 ${⊢}\left({y}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to \left(\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\left({B}\in \mathrm{Fin}\to \left({y}\setminus \left\{{z}\right\}\right)×{B}\in \mathrm{Fin}\right)\to {y}×{B}\in \mathrm{Fin}\right)$
57 56 ex ${⊢}{y}\in \mathrm{Fin}\to \left({B}\in \mathrm{Fin}\to \left(\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\left({B}\in \mathrm{Fin}\to \left({y}\setminus \left\{{z}\right\}\right)×{B}\in \mathrm{Fin}\right)\to {y}×{B}\in \mathrm{Fin}\right)\right)$
58 57 com23 ${⊢}{y}\in \mathrm{Fin}\to \left(\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\left({B}\in \mathrm{Fin}\to \left({y}\setminus \left\{{z}\right\}\right)×{B}\in \mathrm{Fin}\right)\to \left({B}\in \mathrm{Fin}\to {y}×{B}\in \mathrm{Fin}\right)\right)$
59 3 6 9 12 16 58 findcard ${⊢}{A}\in \mathrm{Fin}\to \left({B}\in \mathrm{Fin}\to {A}×{B}\in \mathrm{Fin}\right)$
60 59 imp ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to {A}×{B}\in \mathrm{Fin}$