Metamath Proof Explorer


Theorem redundss3

Description: Implication of redundancy predicate. (Contributed by Peter Mazsa, 26-Oct-2022)

Ref Expression
Hypothesis redundss3.1 𝐷𝐶
Assertion redundss3 ( 𝐴 Redund ⟨ 𝐵 , 𝐶 ⟩ → 𝐴 Redund ⟨ 𝐵 , 𝐷 ⟩ )

Proof

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 ⟨ 𝐵 , 𝐷 ⟩ )