Metamath Proof Explorer

Theorem xpima

Description: Direct image by a Cartesian product. (Contributed by Thierry Arnoux, 4-Feb-2017)

Ref Expression
Assertion xpima ( ( 𝐴 × 𝐵 ) “ 𝐶 ) = if ( ( 𝐴 ∩ 𝐶 ) = ∅ , ∅ , 𝐵 )

Proof

Step Hyp Ref Expression
1 exmid ⊢ ( ( 𝐴 ∩ 𝐶 ) = ∅ ∨ ¬ ( 𝐴 ∩ 𝐶 ) = ∅ )
2 df-ima ⊢ ( ( 𝐴 × 𝐵 ) “ 𝐶 ) = ran ( ( 𝐴 × 𝐵 ) ↾ 𝐶 )
3 df-res ⊢ ( ( 𝐴 × 𝐵 ) ↾ 𝐶 ) = ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × V ) )
4 3 rneqi ⊢ ran ( ( 𝐴 × 𝐵 ) ↾ 𝐶 ) = ran ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × V ) )
5 2 4 eqtri ⊢ ( ( 𝐴 × 𝐵 ) “ 𝐶 ) = ran ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × V ) )
6 inxp ⊢ ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × V ) ) = ( ( 𝐴 ∩ 𝐶 ) × ( 𝐵 ∩ V ) )
7 6 rneqi ⊢ ran ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × V ) ) = ran ( ( 𝐴 ∩ 𝐶 ) × ( 𝐵 ∩ V ) )
8 inv1 ⊢ ( 𝐵 ∩ V ) = 𝐵
9 8 xpeq2i ⊢ ( ( 𝐴 ∩ 𝐶 ) × ( 𝐵 ∩ V ) ) = ( ( 𝐴 ∩ 𝐶 ) × 𝐵 )
10 9 rneqi ⊢ ran ( ( 𝐴 ∩ 𝐶 ) × ( 𝐵 ∩ V ) ) = ran ( ( 𝐴 ∩ 𝐶 ) × 𝐵 )
11 5 7 10 3eqtri ⊢ ( ( 𝐴 × 𝐵 ) “ 𝐶 ) = ran ( ( 𝐴 ∩ 𝐶 ) × 𝐵 )
12 xpeq1 ⊢ ( ( 𝐴 ∩ 𝐶 ) = ∅ → ( ( 𝐴 ∩ 𝐶 ) × 𝐵 ) = ( ∅ × 𝐵 ) )
13 0xp ⊢ ( ∅ × 𝐵 ) = ∅
14 12 13 eqtrdi ⊢ ( ( 𝐴 ∩ 𝐶 ) = ∅ → ( ( 𝐴 ∩ 𝐶 ) × 𝐵 ) = ∅ )
15 14 rneqd ⊢ ( ( 𝐴 ∩ 𝐶 ) = ∅ → ran ( ( 𝐴 ∩ 𝐶 ) × 𝐵 ) = ran ∅ )
16 rn0 ⊢ ran ∅ = ∅
17 15 16 eqtrdi ⊢ ( ( 𝐴 ∩ 𝐶 ) = ∅ → ran ( ( 𝐴 ∩ 𝐶 ) × 𝐵 ) = ∅ )
18 11 17 eqtrid ⊢ ( ( 𝐴 ∩ 𝐶 ) = ∅ → ( ( 𝐴 × 𝐵 ) “ 𝐶 ) = ∅ )
19 18 ancli ⊢ ( ( 𝐴 ∩ 𝐶 ) = ∅ → ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( ( 𝐴 × 𝐵 ) “ 𝐶 ) = ∅ ) )
20 df-ne ⊢ ( ( 𝐴 ∩ 𝐶 ) ≠ ∅ ↔ ¬ ( 𝐴 ∩ 𝐶 ) = ∅ )
21 rnxp ⊢ ( ( 𝐴 ∩ 𝐶 ) ≠ ∅ → ran ( ( 𝐴 ∩ 𝐶 ) × 𝐵 ) = 𝐵 )
22 20 21 sylbir ⊢ ( ¬ ( 𝐴 ∩ 𝐶 ) = ∅ → ran ( ( 𝐴 ∩ 𝐶 ) × 𝐵 ) = 𝐵 )
23 11 22 eqtrid ⊢ ( ¬ ( 𝐴 ∩ 𝐶 ) = ∅ → ( ( 𝐴 × 𝐵 ) “ 𝐶 ) = 𝐵 )
24 23 ancli ⊢ ( ¬ ( 𝐴 ∩ 𝐶 ) = ∅ → ( ¬ ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( ( 𝐴 × 𝐵 ) “ 𝐶 ) = 𝐵 ) )
25 19 24 orim12i ⊢ ( ( ( 𝐴 ∩ 𝐶 ) = ∅ ∨ ¬ ( 𝐴 ∩ 𝐶 ) = ∅ ) → ( ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( ( 𝐴 × 𝐵 ) “ 𝐶 ) = ∅ ) ∨ ( ¬ ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( ( 𝐴 × 𝐵 ) “ 𝐶 ) = 𝐵 ) ) )
26 1 25 ax-mp ⊢ ( ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( ( 𝐴 × 𝐵 ) “ 𝐶 ) = ∅ ) ∨ ( ¬ ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( ( 𝐴 × 𝐵 ) “ 𝐶 ) = 𝐵 ) )
27 eqif ⊢ ( ( ( 𝐴 × 𝐵 ) “ 𝐶 ) = if ( ( 𝐴 ∩ 𝐶 ) = ∅ , ∅ , 𝐵 ) ↔ ( ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( ( 𝐴 × 𝐵 ) “ 𝐶 ) = ∅ ) ∨ ( ¬ ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( ( 𝐴 × 𝐵 ) “ 𝐶 ) = 𝐵 ) ) )
28 26 27 mpbir ⊢ ( ( 𝐴 × 𝐵 ) “ 𝐶 ) = if ( ( 𝐴 ∩ 𝐶 ) = ∅ , ∅ , 𝐵 )