xpfiOLD

Description: Obsolete version of xpfi as of 10-Jan-2025. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 12-Mar-2015) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	xpfiOLD	$⊢ (A \in Fin \land B \in Fin) \to A \times B \in Fin$

Proof

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

Metamath Proof Explorer

Theorem xpfiOLD

Proof