Theorem br1cossinres

Description: B and C are cosets by an intersection with a restriction: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021)

	Ref	Expression
Assertion	br1cossinres	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐵 ≀ ( 𝑅 ∩ ( 𝑆 ↾ 𝐴 ) ) 𝐶 ↔ ∃ 𝑢 ∈ 𝐴 ( ( 𝑢 𝑆 𝐵 ∧ 𝑢 𝑅 𝐵 ) ∧ ( 𝑢 𝑆 𝐶 ∧ 𝑢 𝑅 𝐶 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		inres	⊢ ( 𝑅 ∩ ( 𝑆 ↾ 𝐴 ) ) = ( ( 𝑅 ∩ 𝑆 ) ↾ 𝐴 )
2	1	cosseqi	⊢ ≀ ( 𝑅 ∩ ( 𝑆 ↾ 𝐴 ) ) = ≀ ( ( 𝑅 ∩ 𝑆 ) ↾ 𝐴 )
3	2	breqi	⊢ ( 𝐵 ≀ ( 𝑅 ∩ ( 𝑆 ↾ 𝐴 ) ) 𝐶 ↔ 𝐵 ≀ ( ( 𝑅 ∩ 𝑆 ) ↾ 𝐴 ) 𝐶 )
4		br1cossres	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐵 ≀ ( ( 𝑅 ∩ 𝑆 ) ↾ 𝐴 ) 𝐶 ↔ ∃ 𝑢 ∈ 𝐴 ( 𝑢 ( 𝑅 ∩ 𝑆 ) 𝐵 ∧ 𝑢 ( 𝑅 ∩ 𝑆 ) 𝐶 ) ) )
5		brin	⊢ ( 𝑢 ( 𝑅 ∩ 𝑆 ) 𝐵 ↔ ( 𝑢 𝑅 𝐵 ∧ 𝑢 𝑆 𝐵 ) )
6		brin	⊢ ( 𝑢 ( 𝑅 ∩ 𝑆 ) 𝐶 ↔ ( 𝑢 𝑅 𝐶 ∧ 𝑢 𝑆 𝐶 ) )
7	5 6	anbi12i	⊢ ( ( 𝑢 ( 𝑅 ∩ 𝑆 ) 𝐵 ∧ 𝑢 ( 𝑅 ∩ 𝑆 ) 𝐶 ) ↔ ( ( 𝑢 𝑅 𝐵 ∧ 𝑢 𝑆 𝐵 ) ∧ ( 𝑢 𝑅 𝐶 ∧ 𝑢 𝑆 𝐶 ) ) )
8		an2anr	⊢ ( ( ( 𝑢 𝑅 𝐵 ∧ 𝑢 𝑆 𝐵 ) ∧ ( 𝑢 𝑅 𝐶 ∧ 𝑢 𝑆 𝐶 ) ) ↔ ( ( 𝑢 𝑆 𝐵 ∧ 𝑢 𝑅 𝐵 ) ∧ ( 𝑢 𝑆 𝐶 ∧ 𝑢 𝑅 𝐶 ) ) )
9	7 8	bitri	⊢ ( ( 𝑢 ( 𝑅 ∩ 𝑆 ) 𝐵 ∧ 𝑢 ( 𝑅 ∩ 𝑆 ) 𝐶 ) ↔ ( ( 𝑢 𝑆 𝐵 ∧ 𝑢 𝑅 𝐵 ) ∧ ( 𝑢 𝑆 𝐶 ∧ 𝑢 𝑅 𝐶 ) ) )
10	9	rexbii	⊢ ( ∃ 𝑢 ∈ 𝐴 ( 𝑢 ( 𝑅 ∩ 𝑆 ) 𝐵 ∧ 𝑢 ( 𝑅 ∩ 𝑆 ) 𝐶 ) ↔ ∃ 𝑢 ∈ 𝐴 ( ( 𝑢 𝑆 𝐵 ∧ 𝑢 𝑅 𝐵 ) ∧ ( 𝑢 𝑆 𝐶 ∧ 𝑢 𝑅 𝐶 ) ) )
11	4 10	bitrdi	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐵 ≀ ( ( 𝑅 ∩ 𝑆 ) ↾ 𝐴 ) 𝐶 ↔ ∃ 𝑢 ∈ 𝐴 ( ( 𝑢 𝑆 𝐵 ∧ 𝑢 𝑅 𝐵 ) ∧ ( 𝑢 𝑆 𝐶 ∧ 𝑢 𝑅 𝐶 ) ) ) )
12	3 11	syl5bb	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐵 ≀ ( 𝑅 ∩ ( 𝑆 ↾ 𝐴 ) ) 𝐶 ↔ ∃ 𝑢 ∈ 𝐴 ( ( 𝑢 𝑆 𝐵 ∧ 𝑢 𝑅 𝐵 ) ∧ ( 𝑢 𝑆 𝐶 ∧ 𝑢 𝑅 𝐶 ) ) ) )