This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 imbitrid ⊢ ( 𝐵 ≠ ∅ → ( ( 𝐴 × 𝐵 ) ∈ 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 imbitrid ⊢ ( 𝐴 ≠ ∅ → ( ( 𝐴 × 𝐵 ) ∈ 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 ‘ ( 𝐴 × 𝐵 ) )