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 ⊢ B ∈ V ∧ C ∈ W → B ≀ R ∩ S ↾ A C ↔ ∃ u ∈ A u S B ∧ u R B ∧ u S C ∧ u R C

Proof

Step Hyp Ref Expression
1 inres ⊢ R ∩ S ↾ A = R ∩ S ↾ A
2 1 cosseqi ⊢ ≀ R ∩ S ↾ A = ≀ R ∩ S ↾ A
3 2 breqi ⊢ B ≀ R ∩ S ↾ A C ↔ B ≀ R ∩ S ↾ A C
4 br1cossres ⊢ B ∈ V ∧ C ∈ W → B ≀ R ∩ S ↾ A C ↔ ∃ u ∈ A u R ∩ S B ∧ u R ∩ S C
5 brin ⊢ u R ∩ S B ↔ u R B ∧ u S B
6 brin ⊢ u R ∩ S C ↔ u R C ∧ u S C
7 5 6 anbi12i ⊢ u R ∩ S B ∧ u R ∩ S C ↔ u R B ∧ u S B ∧ u R C ∧ u S C
8 an2anr ⊢ u R B ∧ u S B ∧ u R C ∧ u S C ↔ u S B ∧ u R B ∧ u S C ∧ u R C
9 7 8 bitri ⊢ u R ∩ S B ∧ u R ∩ S C ↔ u S B ∧ u R B ∧ u S C ∧ u R C
10 9 rexbii ⊢ ∃ u ∈ A u R ∩ S B ∧ u R ∩ S C ↔ ∃ u ∈ A u S B ∧ u R B ∧ u S C ∧ u R C
11 4 10 bitrdi ⊢ B ∈ V ∧ C ∈ W → B ≀ R ∩ S ↾ A C ↔ ∃ u ∈ A u S B ∧ u R B ∧ u S C ∧ u R C
12 3 11 syl5bb ⊢ B ∈ V ∧ C ∈ W → B ≀ R ∩ S ↾ A C ↔ ∃ u ∈ A u S B ∧ u R B ∧ u S C ∧ u R C