Step |
Hyp |
Ref |
Expression |
1 |
|
redundss3.1 |
⊢ 𝐷 ⊆ 𝐶 |
2 |
|
ineq1 |
⊢ ( ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) → ( ( 𝐴 ∩ 𝐶 ) ∩ 𝐷 ) = ( ( 𝐵 ∩ 𝐶 ) ∩ 𝐷 ) ) |
3 |
|
dfss |
⊢ ( 𝐷 ⊆ 𝐶 ↔ 𝐷 = ( 𝐷 ∩ 𝐶 ) ) |
4 |
1 3
|
mpbi |
⊢ 𝐷 = ( 𝐷 ∩ 𝐶 ) |
5 |
|
incom |
⊢ ( 𝐷 ∩ 𝐶 ) = ( 𝐶 ∩ 𝐷 ) |
6 |
4 5
|
eqtri |
⊢ 𝐷 = ( 𝐶 ∩ 𝐷 ) |
7 |
6
|
ineq2i |
⊢ ( 𝐴 ∩ 𝐷 ) = ( 𝐴 ∩ ( 𝐶 ∩ 𝐷 ) ) |
8 |
|
inass |
⊢ ( ( 𝐴 ∩ 𝐶 ) ∩ 𝐷 ) = ( 𝐴 ∩ ( 𝐶 ∩ 𝐷 ) ) |
9 |
7 8
|
eqtr4i |
⊢ ( 𝐴 ∩ 𝐷 ) = ( ( 𝐴 ∩ 𝐶 ) ∩ 𝐷 ) |
10 |
6
|
ineq2i |
⊢ ( 𝐵 ∩ 𝐷 ) = ( 𝐵 ∩ ( 𝐶 ∩ 𝐷 ) ) |
11 |
|
inass |
⊢ ( ( 𝐵 ∩ 𝐶 ) ∩ 𝐷 ) = ( 𝐵 ∩ ( 𝐶 ∩ 𝐷 ) ) |
12 |
10 11
|
eqtr4i |
⊢ ( 𝐵 ∩ 𝐷 ) = ( ( 𝐵 ∩ 𝐶 ) ∩ 𝐷 ) |
13 |
2 9 12
|
3eqtr4g |
⊢ ( ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) → ( 𝐴 ∩ 𝐷 ) = ( 𝐵 ∩ 𝐷 ) ) |
14 |
13
|
anim2i |
⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) ) → ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐷 ) = ( 𝐵 ∩ 𝐷 ) ) ) |
15 |
|
df-redund |
⊢ ( 𝐴 Redund 〈 𝐵 , 𝐶 〉 ↔ ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) ) ) |
16 |
|
df-redund |
⊢ ( 𝐴 Redund 〈 𝐵 , 𝐷 〉 ↔ ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐷 ) = ( 𝐵 ∩ 𝐷 ) ) ) |
17 |
14 15 16
|
3imtr4i |
⊢ ( 𝐴 Redund 〈 𝐵 , 𝐶 〉 → 𝐴 Redund 〈 𝐵 , 𝐷 〉 ) |