Theorem txindislem 23520

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

Assertion

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

Proof of Theorem txindislem

Step	Hyp	Ref	Expression
1		0xp 5737	. . 3 ⊢ (∅ × ( I ‘𝐵)) = ∅
2		fvprc 6850	. . . 4 ⊢ (¬ 𝐴 ∈ V → ( I ‘𝐴) = ∅)
3	2	xpeq1d 5667	. . 3 ⊢ (¬ 𝐴 ∈ V → (( I ‘𝐴) × ( I ‘𝐵)) = (∅ × ( I ‘𝐵)))
4		simpr 484	. . . . . . . 8 ⊢ ((¬ 𝐴 ∈ V ∧ 𝐵 = ∅) → 𝐵 = ∅)
5	4	xpeq2d 5668	. . . . . . 7 ⊢ ((¬ 𝐴 ∈ V ∧ 𝐵 = ∅) → (𝐴 × 𝐵) = (𝐴 × ∅))
6		xp0 6131	. . . . . . 7 ⊢ (𝐴 × ∅) = ∅
7	5, 6	eqtrdi 2780	. . . . . 6 ⊢ ((¬ 𝐴 ∈ V ∧ 𝐵 = ∅) → (𝐴 × 𝐵) = ∅)
8	7	fveq2d 6862	. . . . 5 ⊢ ((¬ 𝐴 ∈ V ∧ 𝐵 = ∅) → ( I ‘(𝐴 × 𝐵)) = ( I ‘∅))
9		0ex 5262	. . . . . 6 ⊢ ∅ ∈ V
10		fvi 6937	. . . . . 6 ⊢ (∅ ∈ V → ( I ‘∅) = ∅)
11	9, 10	ax-mp 5	. . . . 5 ⊢ ( I ‘∅) = ∅
12	8, 11	eqtrdi 2780	. . . 4 ⊢ ((¬ 𝐴 ∈ V ∧ 𝐵 = ∅) → ( I ‘(𝐴 × 𝐵)) = ∅)
13		dmexg 7877	. . . . . . . 8 ⊢ ((𝐴 × 𝐵) ∈ V → dom (𝐴 × 𝐵) ∈ V)
14		dmxp 5892	. . . . . . . . 9 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
15	14	eleq1d 2813	. . . . . . . 8 ⊢ (𝐵 ≠ ∅ → (dom (𝐴 × 𝐵) ∈ V ↔ 𝐴 ∈ V))
16	13, 15	imbitrid 244	. . . . . . 7 ⊢ (𝐵 ≠ ∅ → ((𝐴 × 𝐵) ∈ V → 𝐴 ∈ V))
17	16	con3d 152	. . . . . 6 ⊢ (𝐵 ≠ ∅ → (¬ 𝐴 ∈ V → ¬ (𝐴 × 𝐵) ∈ V))
18	17	impcom 407	. . . . 5 ⊢ ((¬ 𝐴 ∈ V ∧ 𝐵 ≠ ∅) → ¬ (𝐴 × 𝐵) ∈ V)
19		fvprc 6850	. . . . 5 ⊢ (¬ (𝐴 × 𝐵) ∈ V → ( I ‘(𝐴 × 𝐵)) = ∅)
20	18, 19	syl 17	. . . 4 ⊢ ((¬ 𝐴 ∈ V ∧ 𝐵 ≠ ∅) → ( I ‘(𝐴 × 𝐵)) = ∅)
21	12, 20	pm2.61dane 3012	. . 3 ⊢ (¬ 𝐴 ∈ V → ( I ‘(𝐴 × 𝐵)) = ∅)
22	1, 3, 21	3eqtr4a 2790	. 2 ⊢ (¬ 𝐴 ∈ V → (( I ‘𝐴) × ( I ‘𝐵)) = ( I ‘(𝐴 × 𝐵)))
23		xp0 6131	. . 3 ⊢ (( I ‘𝐴) × ∅) = ∅
24		fvprc 6850	. . . 4 ⊢ (¬ 𝐵 ∈ V → ( I ‘𝐵) = ∅)
25	24	xpeq2d 5668	. . 3 ⊢ (¬ 𝐵 ∈ V → (( I ‘𝐴) × ( I ‘𝐵)) = (( I ‘𝐴) × ∅))
26		simpr 484	. . . . . . . 8 ⊢ ((¬ 𝐵 ∈ V ∧ 𝐴 = ∅) → 𝐴 = ∅)
27	26	xpeq1d 5667	. . . . . . 7 ⊢ ((¬ 𝐵 ∈ V ∧ 𝐴 = ∅) → (𝐴 × 𝐵) = (∅ × 𝐵))
28		0xp 5737	. . . . . . 7 ⊢ (∅ × 𝐵) = ∅
29	27, 28	eqtrdi 2780	. . . . . 6 ⊢ ((¬ 𝐵 ∈ V ∧ 𝐴 = ∅) → (𝐴 × 𝐵) = ∅)
30	29	fveq2d 6862	. . . . 5 ⊢ ((¬ 𝐵 ∈ V ∧ 𝐴 = ∅) → ( I ‘(𝐴 × 𝐵)) = ( I ‘∅))
31	30, 11	eqtrdi 2780	. . . 4 ⊢ ((¬ 𝐵 ∈ V ∧ 𝐴 = ∅) → ( I ‘(𝐴 × 𝐵)) = ∅)
32		rnexg 7878	. . . . . . . 8 ⊢ ((𝐴 × 𝐵) ∈ V → ran (𝐴 × 𝐵) ∈ V)
33		rnxp 6143	. . . . . . . . 9 ⊢ (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵)
34	33	eleq1d 2813	. . . . . . . 8 ⊢ (𝐴 ≠ ∅ → (ran (𝐴 × 𝐵) ∈ V ↔ 𝐵 ∈ V))
35	32, 34	imbitrid 244	. . . . . . 7 ⊢ (𝐴 ≠ ∅ → ((𝐴 × 𝐵) ∈ V → 𝐵 ∈ V))
36	35	con3d 152	. . . . . 6 ⊢ (𝐴 ≠ ∅ → (¬ 𝐵 ∈ V → ¬ (𝐴 × 𝐵) ∈ V))
37	36	impcom 407	. . . . 5 ⊢ ((¬ 𝐵 ∈ V ∧ 𝐴 ≠ ∅) → ¬ (𝐴 × 𝐵) ∈ V)
38	37, 19	syl 17	. . . 4 ⊢ ((¬ 𝐵 ∈ V ∧ 𝐴 ≠ ∅) → ( I ‘(𝐴 × 𝐵)) = ∅)
39	31, 38	pm2.61dane 3012	. . 3 ⊢ (¬ 𝐵 ∈ V → ( I ‘(𝐴 × 𝐵)) = ∅)
40	23, 25, 39	3eqtr4a 2790	. 2 ⊢ (¬ 𝐵 ∈ V → (( I ‘𝐴) × ( I ‘𝐵)) = ( I ‘(𝐴 × 𝐵)))
41		fvi 6937	. . . 4 ⊢ (𝐴 ∈ V → ( I ‘𝐴) = 𝐴)
42		fvi 6937	. . . 4 ⊢ (𝐵 ∈ V → ( I ‘𝐵) = 𝐵)
43		xpeq12 5663	. . . 4 ⊢ ((( I ‘𝐴) = 𝐴 ∧ ( I ‘𝐵) = 𝐵) → (( I ‘𝐴) × ( I ‘𝐵)) = (𝐴 × 𝐵))
44	41, 42, 43	syl2an 596	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (( I ‘𝐴) × ( I ‘𝐵)) = (𝐴 × 𝐵))
45		xpexg 7726	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 × 𝐵) ∈ V)
46		fvi 6937	. . . 4 ⊢ ((𝐴 × 𝐵) ∈ V → ( I ‘(𝐴 × 𝐵)) = (𝐴 × 𝐵))
47	45, 46	syl 17	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ( I ‘(𝐴 × 𝐵)) = (𝐴 × 𝐵))
48	44, 47	eqtr4d 2767	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (( I ‘𝐴) × ( I ‘𝐵)) = ( I ‘(𝐴 × 𝐵)))
49	22, 40, 48	ecase 1033	1 ⊢ (( I ‘𝐴) × ( I ‘𝐵)) = ( I ‘(𝐴 × 𝐵))

Syntax hints:  ¬ wn 3   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  Vcvv 3447  ∅c0 4296   I cid 5532   × cxp 5636  dom cdm 5638  ran crn 5639  ‘cfv 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fv 6519

This theorem is referenced by:  txindis  23521