Metamath Proof Explorer

Theorem br1cossxrnres

Description: <. B , C >. and <. D , E >. are cosets by an range Cartesian product 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 bitrid ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) ∧ ( 𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) ) → ( ⟨ 𝐵 , 𝐶 ⟩ ≀ ( ( 𝑅 ⋉ 𝑆 ) ↾ 𝐴 ) ⟨ 𝐷 , 𝐸 ⟩ ↔ ∃ 𝑢 ∈ 𝐴 ( ( 𝑢 𝑆 𝐶 ∧ 𝑢 𝑅 𝐵 ) ∧ ( 𝑢 𝑆 𝐸 ∧ 𝑢 𝑅 𝐷 ) ) ) )
17 3 16 bitr3id ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) ∧ ( 𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) ) → ( ⟨ 𝐵 , 𝐶 ⟩ ≀ ( 𝑅 ⋉ ( 𝑆 ↾ 𝐴 ) ) ⟨ 𝐷 , 𝐸 ⟩ ↔ ∃ 𝑢 ∈ 𝐴 ( ( 𝑢 𝑆 𝐶 ∧ 𝑢 𝑅 𝐵 ) ∧ ( 𝑢 𝑆 𝐸 ∧ 𝑢 𝑅 𝐷 ) ) ) )