Proof of Theorem redundss3
Step | Hyp | Ref
| Expression |
1 | | ineq1 4135 |
. . . 4
⊢ ((𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶) → ((𝐴 ∩ 𝐶) ∩ 𝐷) = ((𝐵 ∩ 𝐶) ∩ 𝐷)) |
2 | | redundss3.1 |
. . . . . . . 8
⊢ 𝐷 ⊆ 𝐶 |
3 | | dfss 3899 |
. . . . . . . 8
⊢ (𝐷 ⊆ 𝐶 ↔ 𝐷 = (𝐷 ∩ 𝐶)) |
4 | 2, 3 | mpbi 233 |
. . . . . . 7
⊢ 𝐷 = (𝐷 ∩ 𝐶) |
5 | | incom 4130 |
. . . . . . 7
⊢ (𝐷 ∩ 𝐶) = (𝐶 ∩ 𝐷) |
6 | 4, 5 | eqtri 2766 |
. . . . . 6
⊢ 𝐷 = (𝐶 ∩ 𝐷) |
7 | 6 | ineq2i 4139 |
. . . . 5
⊢ (𝐴 ∩ 𝐷) = (𝐴 ∩ (𝐶 ∩ 𝐷)) |
8 | | inass 4149 |
. . . . 5
⊢ ((𝐴 ∩ 𝐶) ∩ 𝐷) = (𝐴 ∩ (𝐶 ∩ 𝐷)) |
9 | 7, 8 | eqtr4i 2769 |
. . . 4
⊢ (𝐴 ∩ 𝐷) = ((𝐴 ∩ 𝐶) ∩ 𝐷) |
10 | 6 | ineq2i 4139 |
. . . . 5
⊢ (𝐵 ∩ 𝐷) = (𝐵 ∩ (𝐶 ∩ 𝐷)) |
11 | | inass 4149 |
. . . . 5
⊢ ((𝐵 ∩ 𝐶) ∩ 𝐷) = (𝐵 ∩ (𝐶 ∩ 𝐷)) |
12 | 10, 11 | eqtr4i 2769 |
. . . 4
⊢ (𝐵 ∩ 𝐷) = ((𝐵 ∩ 𝐶) ∩ 𝐷) |
13 | 1, 9, 12 | 3eqtr4g 2804 |
. . 3
⊢ ((𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶) → (𝐴 ∩ 𝐷) = (𝐵 ∩ 𝐷)) |
14 | 13 | anim2i 620 |
. 2
⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) → (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐷) = (𝐵 ∩ 𝐷))) |
15 | | df-redund 36504 |
. 2
⊢ (𝐴 Redund 〈𝐵, 𝐶〉 ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))) |
16 | | df-redund 36504 |
. 2
⊢ (𝐴 Redund 〈𝐵, 𝐷〉 ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐷) = (𝐵 ∩ 𝐷))) |
17 | 14, 15, 16 | 3imtr4i 295 |
1
⊢ (𝐴 Redund 〈𝐵, 𝐶〉 → 𝐴 Redund 〈𝐵, 𝐷〉) |