This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 bitrid ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐵 ≀ ( 𝑅 ∩ ( 𝑆 ↾ 𝐴 ) ) 𝐶 ↔ ∃ 𝑢 ∈ 𝐴 ( ( 𝑢 𝑆 𝐵 ∧ 𝑢 𝑅 𝐵 ) ∧ ( 𝑢 𝑆 𝐶 ∧ 𝑢 𝑅 𝐶 ) ) ) )