Theorem br1cossxrnres

Description: <. B , C >. and <. D , E >. are cosets by an intersection with a restriction: a binary relation. (Contributed by Peter Mazsa, 8-Jun-2021)

	Ref	Expression
Assertion	br1cossxrnres	⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) ∧ ( 𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) ) → ( ⟨ 𝐵 , 𝐶 ⟩ ≀ ( 𝑅 ⋉ ( 𝑆 ↾ 𝐴 ) ) ⟨ 𝐷 , 𝐸 ⟩ ↔ ∃ 𝑢 ∈ 𝐴 ( ( 𝑢 𝑆 𝐶 ∧ 𝑢 𝑅 𝐵 ) ∧ ( 𝑢 𝑆 𝐸 ∧ 𝑢 𝑅 𝐷 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		xrnres2	⊢ ( ( 𝑅 ⋉ 𝑆 ) ↾ 𝐴 ) = ( 𝑅 ⋉ ( 𝑆 ↾ 𝐴 ) )
2	1	cosseqi	⊢ ≀ ( ( 𝑅 ⋉ 𝑆 ) ↾ 𝐴 ) = ≀ ( 𝑅 ⋉ ( 𝑆 ↾ 𝐴 ) )
3	2	breqi	⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ≀ ( ( 𝑅 ⋉ 𝑆 ) ↾ 𝐴 ) ⟨ 𝐷 , 𝐸 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ ≀ ( 𝑅 ⋉ ( 𝑆 ↾ 𝐴 ) ) ⟨ 𝐷 , 𝐸 ⟩ )
4		opex	⊢ ⟨ 𝐵 , 𝐶 ⟩ ∈ V
5		opex	⊢ ⟨ 𝐷 , 𝐸 ⟩ ∈ V
6		br1cossres	⊢ ( ( ⟨ 𝐵 , 𝐶 ⟩ ∈ V ∧ ⟨ 𝐷 , 𝐸 ⟩ ∈ V ) → ( ⟨ 𝐵 , 𝐶 ⟩ ≀ ( ( 𝑅 ⋉ 𝑆 ) ↾ 𝐴 ) ⟨ 𝐷 , 𝐸 ⟩ ↔ ∃ 𝑢 ∈ 𝐴 ( 𝑢 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝐵 , 𝐶 ⟩ ∧ 𝑢 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝐷 , 𝐸 ⟩ ) ) )
7	4 5 6	mp2an	⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ≀ ( ( 𝑅 ⋉ 𝑆 ) ↾ 𝐴 ) ⟨ 𝐷 , 𝐸 ⟩ ↔ ∃ 𝑢 ∈ 𝐴 ( 𝑢 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝐵 , 𝐶 ⟩ ∧ 𝑢 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝐷 , 𝐸 ⟩ ) )
8		brxrn	⊢ ( ( 𝑢 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝑢 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝑢 𝑅 𝐵 ∧ 𝑢 𝑆 𝐶 ) ) )
9	8	el3v1	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝑢 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝑢 𝑅 𝐵 ∧ 𝑢 𝑆 𝐶 ) ) )
10		brxrn	⊢ ( ( 𝑢 ∈ V ∧ 𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( 𝑢 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝐷 , 𝐸 ⟩ ↔ ( 𝑢 𝑅 𝐷 ∧ 𝑢 𝑆 𝐸 ) ) )
11	10	el3v1	⊢ ( ( 𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( 𝑢 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝐷 , 𝐸 ⟩ ↔ ( 𝑢 𝑅 𝐷 ∧ 𝑢 𝑆 𝐸 ) ) )
12	9 11	bi2anan9	⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) ∧ ( 𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) ) → ( ( 𝑢 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝐵 , 𝐶 ⟩ ∧ 𝑢 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝐷 , 𝐸 ⟩ ) ↔ ( ( 𝑢 𝑅 𝐵 ∧ 𝑢 𝑆 𝐶 ) ∧ ( 𝑢 𝑅 𝐷 ∧ 𝑢 𝑆 𝐸 ) ) ) )
13		an2anr	⊢ ( ( ( 𝑢 𝑅 𝐵 ∧ 𝑢 𝑆 𝐶 ) ∧ ( 𝑢 𝑅 𝐷 ∧ 𝑢 𝑆 𝐸 ) ) ↔ ( ( 𝑢 𝑆 𝐶 ∧ 𝑢 𝑅 𝐵 ) ∧ ( 𝑢 𝑆 𝐸 ∧ 𝑢 𝑅 𝐷 ) ) )
14	12 13	bitrdi	⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) ∧ ( 𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) ) → ( ( 𝑢 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝐵 , 𝐶 ⟩ ∧ 𝑢 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝐷 , 𝐸 ⟩ ) ↔ ( ( 𝑢 𝑆 𝐶 ∧ 𝑢 𝑅 𝐵 ) ∧ ( 𝑢 𝑆 𝐸 ∧ 𝑢 𝑅 𝐷 ) ) ) )
15	14	rexbidv	⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) ∧ ( 𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) ) → ( ∃ 𝑢 ∈ 𝐴 ( 𝑢 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝐵 , 𝐶 ⟩ ∧ 𝑢 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝐷 , 𝐸 ⟩ ) ↔ ∃ 𝑢 ∈ 𝐴 ( ( 𝑢 𝑆 𝐶 ∧ 𝑢 𝑅 𝐵 ) ∧ ( 𝑢 𝑆 𝐸 ∧ 𝑢 𝑅 𝐷 ) ) ) )
16	7 15	syl5bb	⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) ∧ ( 𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) ) → ( ⟨ 𝐵 , 𝐶 ⟩ ≀ ( ( 𝑅 ⋉ 𝑆 ) ↾ 𝐴 ) ⟨ 𝐷 , 𝐸 ⟩ ↔ ∃ 𝑢 ∈ 𝐴 ( ( 𝑢 𝑆 𝐶 ∧ 𝑢 𝑅 𝐵 ) ∧ ( 𝑢 𝑆 𝐸 ∧ 𝑢 𝑅 𝐷 ) ) ) )
17	3 16	bitr3id	⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) ∧ ( 𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) ) → ( ⟨ 𝐵 , 𝐶 ⟩ ≀ ( 𝑅 ⋉ ( 𝑆 ↾ 𝐴 ) ) ⟨ 𝐷 , 𝐸 ⟩ ↔ ∃ 𝑢 ∈ 𝐴 ( ( 𝑢 𝑆 𝐶 ∧ 𝑢 𝑅 𝐵 ) ∧ ( 𝑢 𝑆 𝐸 ∧ 𝑢 𝑅 𝐷 ) ) ) )