Theorem txindislem

Description: Lemma for txindis . (Contributed by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Assertion	txindislem	⊢ ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) = ( I ‘ ( 𝐴 × 𝐵 ) )

Proof

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