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