Proof of Theorem xpriindi
| Step | Hyp | Ref
| Expression |
| 1 | | iineq1 5009 |
. . . . . . 7
⊢ (𝐴 = ∅ → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ ∅ 𝐵) |
| 2 | | 0iin 5064 |
. . . . . . 7
⊢ ∩ 𝑥 ∈ ∅ 𝐵 = V |
| 3 | 1, 2 | eqtrdi 2793 |
. . . . . 6
⊢ (𝐴 = ∅ → ∩ 𝑥 ∈ 𝐴 𝐵 = V) |
| 4 | 3 | ineq2d 4220 |
. . . . 5
⊢ (𝐴 = ∅ → (𝐷 ∩ ∩ 𝑥 ∈ 𝐴 𝐵) = (𝐷 ∩ V)) |
| 5 | | inv1 4398 |
. . . . 5
⊢ (𝐷 ∩ V) = 𝐷 |
| 6 | 4, 5 | eqtrdi 2793 |
. . . 4
⊢ (𝐴 = ∅ → (𝐷 ∩ ∩ 𝑥 ∈ 𝐴 𝐵) = 𝐷) |
| 7 | 6 | xpeq2d 5715 |
. . 3
⊢ (𝐴 = ∅ → (𝐶 × (𝐷 ∩ ∩
𝑥 ∈ 𝐴 𝐵)) = (𝐶 × 𝐷)) |
| 8 | | iineq1 5009 |
. . . . . 6
⊢ (𝐴 = ∅ → ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵) = ∩
𝑥 ∈ ∅ (𝐶 × 𝐵)) |
| 9 | | 0iin 5064 |
. . . . . 6
⊢ ∩ 𝑥 ∈ ∅ (𝐶 × 𝐵) = V |
| 10 | 8, 9 | eqtrdi 2793 |
. . . . 5
⊢ (𝐴 = ∅ → ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵) = V) |
| 11 | 10 | ineq2d 4220 |
. . . 4
⊢ (𝐴 = ∅ → ((𝐶 × 𝐷) ∩ ∩
𝑥 ∈ 𝐴 (𝐶 × 𝐵)) = ((𝐶 × 𝐷) ∩ V)) |
| 12 | | inv1 4398 |
. . . 4
⊢ ((𝐶 × 𝐷) ∩ V) = (𝐶 × 𝐷) |
| 13 | 11, 12 | eqtrdi 2793 |
. . 3
⊢ (𝐴 = ∅ → ((𝐶 × 𝐷) ∩ ∩
𝑥 ∈ 𝐴 (𝐶 × 𝐵)) = (𝐶 × 𝐷)) |
| 14 | 7, 13 | eqtr4d 2780 |
. 2
⊢ (𝐴 = ∅ → (𝐶 × (𝐷 ∩ ∩
𝑥 ∈ 𝐴 𝐵)) = ((𝐶 × 𝐷) ∩ ∩
𝑥 ∈ 𝐴 (𝐶 × 𝐵))) |
| 15 | | xpindi 5844 |
. . 3
⊢ (𝐶 × (𝐷 ∩ ∩
𝑥 ∈ 𝐴 𝐵)) = ((𝐶 × 𝐷) ∩ (𝐶 × ∩
𝑥 ∈ 𝐴 𝐵)) |
| 16 | | xpiindi 5846 |
. . . 4
⊢ (𝐴 ≠ ∅ → (𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵) = ∩
𝑥 ∈ 𝐴 (𝐶 × 𝐵)) |
| 17 | 16 | ineq2d 4220 |
. . 3
⊢ (𝐴 ≠ ∅ → ((𝐶 × 𝐷) ∩ (𝐶 × ∩
𝑥 ∈ 𝐴 𝐵)) = ((𝐶 × 𝐷) ∩ ∩
𝑥 ∈ 𝐴 (𝐶 × 𝐵))) |
| 18 | 15, 17 | eqtrid 2789 |
. 2
⊢ (𝐴 ≠ ∅ → (𝐶 × (𝐷 ∩ ∩
𝑥 ∈ 𝐴 𝐵)) = ((𝐶 × 𝐷) ∩ ∩
𝑥 ∈ 𝐴 (𝐶 × 𝐵))) |
| 19 | 14, 18 | pm2.61ine 3025 |
1
⊢ (𝐶 × (𝐷 ∩ ∩
𝑥 ∈ 𝐴 𝐵)) = ((𝐶 × 𝐷) ∩ ∩
𝑥 ∈ 𝐴 (𝐶 × 𝐵)) |