Step | Hyp | Ref
| Expression |
1 | | exmid 894 |
. . 3
⊢ ((𝐴 ∩ 𝐶) = ∅ ∨ ¬ (𝐴 ∩ 𝐶) = ∅) |
2 | | df-ima 5650 |
. . . . . . . 8
⊢ ((𝐴 × 𝐵) “ 𝐶) = ran ((𝐴 × 𝐵) ↾ 𝐶) |
3 | | df-res 5649 |
. . . . . . . . 9
⊢ ((𝐴 × 𝐵) ↾ 𝐶) = ((𝐴 × 𝐵) ∩ (𝐶 × V)) |
4 | 3 | rneqi 5896 |
. . . . . . . 8
⊢ ran
((𝐴 × 𝐵) ↾ 𝐶) = ran ((𝐴 × 𝐵) ∩ (𝐶 × V)) |
5 | 2, 4 | eqtri 2761 |
. . . . . . 7
⊢ ((𝐴 × 𝐵) “ 𝐶) = ran ((𝐴 × 𝐵) ∩ (𝐶 × V)) |
6 | | inxp 5792 |
. . . . . . . 8
⊢ ((𝐴 × 𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ 𝐶) × (𝐵 ∩ V)) |
7 | 6 | rneqi 5896 |
. . . . . . 7
⊢ ran
((𝐴 × 𝐵) ∩ (𝐶 × V)) = ran ((𝐴 ∩ 𝐶) × (𝐵 ∩ V)) |
8 | | inv1 4358 |
. . . . . . . . 9
⊢ (𝐵 ∩ V) = 𝐵 |
9 | 8 | xpeq2i 5664 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝐶) × (𝐵 ∩ V)) = ((𝐴 ∩ 𝐶) × 𝐵) |
10 | 9 | rneqi 5896 |
. . . . . . 7
⊢ ran
((𝐴 ∩ 𝐶) × (𝐵 ∩ V)) = ran ((𝐴 ∩ 𝐶) × 𝐵) |
11 | 5, 7, 10 | 3eqtri 2765 |
. . . . . 6
⊢ ((𝐴 × 𝐵) “ 𝐶) = ran ((𝐴 ∩ 𝐶) × 𝐵) |
12 | | xpeq1 5651 |
. . . . . . . . 9
⊢ ((𝐴 ∩ 𝐶) = ∅ → ((𝐴 ∩ 𝐶) × 𝐵) = (∅ × 𝐵)) |
13 | | 0xp 5734 |
. . . . . . . . 9
⊢ (∅
× 𝐵) =
∅ |
14 | 12, 13 | eqtrdi 2789 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝐶) = ∅ → ((𝐴 ∩ 𝐶) × 𝐵) = ∅) |
15 | 14 | rneqd 5897 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐶) = ∅ → ran ((𝐴 ∩ 𝐶) × 𝐵) = ran ∅) |
16 | | rn0 5885 |
. . . . . . 7
⊢ ran
∅ = ∅ |
17 | 15, 16 | eqtrdi 2789 |
. . . . . 6
⊢ ((𝐴 ∩ 𝐶) = ∅ → ran ((𝐴 ∩ 𝐶) × 𝐵) = ∅) |
18 | 11, 17 | eqtrid 2785 |
. . . . 5
⊢ ((𝐴 ∩ 𝐶) = ∅ → ((𝐴 × 𝐵) “ 𝐶) = ∅) |
19 | 18 | ancli 550 |
. . . 4
⊢ ((𝐴 ∩ 𝐶) = ∅ → ((𝐴 ∩ 𝐶) = ∅ ∧ ((𝐴 × 𝐵) “ 𝐶) = ∅)) |
20 | | df-ne 2941 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐶) ≠ ∅ ↔ ¬ (𝐴 ∩ 𝐶) = ∅) |
21 | | rnxp 6126 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐶) ≠ ∅ → ran ((𝐴 ∩ 𝐶) × 𝐵) = 𝐵) |
22 | 20, 21 | sylbir 234 |
. . . . . 6
⊢ (¬
(𝐴 ∩ 𝐶) = ∅ → ran ((𝐴 ∩ 𝐶) × 𝐵) = 𝐵) |
23 | 11, 22 | eqtrid 2785 |
. . . . 5
⊢ (¬
(𝐴 ∩ 𝐶) = ∅ → ((𝐴 × 𝐵) “ 𝐶) = 𝐵) |
24 | 23 | ancli 550 |
. . . 4
⊢ (¬
(𝐴 ∩ 𝐶) = ∅ → (¬ (𝐴 ∩ 𝐶) = ∅ ∧ ((𝐴 × 𝐵) “ 𝐶) = 𝐵)) |
25 | 19, 24 | orim12i 908 |
. . 3
⊢ (((𝐴 ∩ 𝐶) = ∅ ∨ ¬ (𝐴 ∩ 𝐶) = ∅) → (((𝐴 ∩ 𝐶) = ∅ ∧ ((𝐴 × 𝐵) “ 𝐶) = ∅) ∨ (¬ (𝐴 ∩ 𝐶) = ∅ ∧ ((𝐴 × 𝐵) “ 𝐶) = 𝐵))) |
26 | 1, 25 | ax-mp 5 |
. 2
⊢ (((𝐴 ∩ 𝐶) = ∅ ∧ ((𝐴 × 𝐵) “ 𝐶) = ∅) ∨ (¬ (𝐴 ∩ 𝐶) = ∅ ∧ ((𝐴 × 𝐵) “ 𝐶) = 𝐵)) |
27 | | eqif 4531 |
. 2
⊢ (((𝐴 × 𝐵) “ 𝐶) = if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵) ↔ (((𝐴 ∩ 𝐶) = ∅ ∧ ((𝐴 × 𝐵) “ 𝐶) = ∅) ∨ (¬ (𝐴 ∩ 𝐶) = ∅ ∧ ((𝐴 × 𝐵) “ 𝐶) = 𝐵))) |
28 | 26, 27 | mpbir 230 |
1
⊢ ((𝐴 × 𝐵) “ 𝐶) = if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵) |