txindislem

		Ref	Expression
	Assertion	txindislem	$⊢ I (A) \times I (B) = I (A \times B)$

Proof

Step	Hyp	Ref	Expression
1		0xp	$⊢ \emptyset \times I (B) = \emptyset$
2		fvprc	$⊢ \neg A \in V \to I (A) = \emptyset$
3	2	xpeq1d	$⊢ \neg A \in V \to I (A) \times I (B) = \emptyset \times I (B)$
4		simpr	$⊢ (\neg A \in V \land B = \emptyset) \to B = \emptyset$
5	4	xpeq2d	$⊢ (\neg A \in V \land B = \emptyset) \to A \times B = A \times \emptyset$
6		xp0	$⊢ A \times \emptyset = \emptyset$
7	5 6	eqtrdi	$⊢ (\neg A \in V \land B = \emptyset) \to A \times B = \emptyset$
8	7	fveq2d	$⊢ (\neg A \in V \land B = \emptyset) \to I (A \times B) = I (\emptyset)$
9		0ex	$⊢ \emptyset \in V$
10		fvi	$⊢ \emptyset \in V \to I (\emptyset) = \emptyset$
11	9 10	ax-mp	$⊢ I (\emptyset) = \emptyset$
12	8 11	eqtrdi	$⊢ (\neg A \in V \land B = \emptyset) \to I (A \times B) = \emptyset$
13		dmexg	$⊢ A \times B \in V \to dom (A \times B) \in V$
14		dmxp	$⊢ B \neq \emptyset \to dom (A \times B) = A$
15	14	eleq1d	$⊢ B \neq \emptyset \to (dom (A \times B) \in V \leftrightarrow A \in V)$
16	13 15	syl5ib	$⊢ B \neq \emptyset \to (A \times B \in V \to A \in V)$
17	16	con3d	$⊢ B \neq \emptyset \to (\neg A \in V \to \neg A \times B \in V)$
18	17	impcom	$⊢ (\neg A \in V \land B \neq \emptyset) \to \neg A \times B \in V$
19		fvprc	$⊢ \neg A \times B \in V \to I (A \times B) = \emptyset$
20	18 19	syl	$⊢ (\neg A \in V \land B \neq \emptyset) \to I (A \times B) = \emptyset$
21	12 20	pm2.61dane	$⊢ \neg A \in V \to I (A \times B) = \emptyset$
22	1 3 21	3eqtr4a	$⊢ \neg A \in V \to I (A) \times I (B) = I (A \times B)$
23		xp0	$⊢ I (A) \times \emptyset = \emptyset$
24		fvprc	$⊢ \neg B \in V \to I (B) = \emptyset$
25	24	xpeq2d	$⊢ \neg B \in V \to I (A) \times I (B) = I (A) \times \emptyset$
26		simpr	$⊢ (\neg B \in V \land A = \emptyset) \to A = \emptyset$
27	26	xpeq1d	$⊢ (\neg B \in V \land A = \emptyset) \to A \times B = \emptyset \times B$
28		0xp	$⊢ \emptyset \times B = \emptyset$
29	27 28	eqtrdi	$⊢ (\neg B \in V \land A = \emptyset) \to A \times B = \emptyset$
30	29	fveq2d	$⊢ (\neg B \in V \land A = \emptyset) \to I (A \times B) = I (\emptyset)$
31	30 11	eqtrdi	$⊢ (\neg B \in V \land A = \emptyset) \to I (A \times B) = \emptyset$
32		rnexg	$⊢ A \times B \in V \to ran (A \times B) \in V$
33		rnxp	$⊢ A \neq \emptyset \to ran (A \times B) = B$
34	33	eleq1d	$⊢ A \neq \emptyset \to (ran (A \times B) \in V \leftrightarrow B \in V)$
35	32 34	syl5ib	$⊢ A \neq \emptyset \to (A \times B \in V \to B \in V)$
36	35	con3d	$⊢ A \neq \emptyset \to (\neg B \in V \to \neg A \times B \in V)$
37	36	impcom	$⊢ (\neg B \in V \land A \neq \emptyset) \to \neg A \times B \in V$
38	37 19	syl	$⊢ (\neg B \in V \land A \neq \emptyset) \to I (A \times B) = \emptyset$
39	31 38	pm2.61dane	$⊢ \neg B \in V \to I (A \times B) = \emptyset$
40	23 25 39	3eqtr4a	$⊢ \neg B \in V \to I (A) \times I (B) = I (A \times B)$
41		fvi	$⊢ A \in V \to I (A) = A$
42		fvi	$⊢ B \in V \to I (B) = B$
43		xpeq12	$⊢ (I (A) = A \land I (B) = B) \to I (A) \times I (B) = A \times B$
44	41 42 43	syl2an	$⊢ (A \in V \land B \in V) \to I (A) \times I (B) = A \times B$
45		xpexg	$⊢ (A \in V \land B \in V) \to A \times B \in V$
46		fvi	$⊢ A \times B \in V \to I (A \times B) = A \times B$
47	45 46	syl	$⊢ (A \in V \land B \in V) \to I (A \times B) = A \times B$
48	44 47	eqtr4d	$⊢ (A \in V \land B \in V) \to I (A) \times I (B) = I (A \times B)$
49	22 40 48	ecase	$⊢ I (A) \times I (B) = I (A \times B)$

Metamath Proof Explorer

Theorem txindislem

Proof