Theorem 1cossres

Description: The class of cosets by a restriction. (Contributed by Peter Mazsa, 20-Apr-2019)

	Ref	Expression
Assertion	1cossres	⊢ ≀ ( 𝑅 ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) }

Proof

Step	Hyp	Ref	Expression
1		df-coss	⊢ ≀ ( 𝑅 ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑥 ∧ 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑦 ) }
2		df-rex	⊢ ( ∃ 𝑢 ∈ 𝐴 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) ↔ ∃ 𝑢 ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) ) )
3		anandi	⊢ ( ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) ) ↔ ( ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 𝑥 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 𝑦 ) ) )
4		brres	⊢ ( 𝑥 ∈ V → ( 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑥 ↔ ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 𝑥 ) ) )
5	4	elv	⊢ ( 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑥 ↔ ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 𝑥 ) )
6		brres	⊢ ( 𝑦 ∈ V → ( 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑦 ↔ ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 𝑦 ) ) )
7	6	elv	⊢ ( 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑦 ↔ ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 𝑦 ) )
8	5 7	anbi12i	⊢ ( ( 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑥 ∧ 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑦 ) ↔ ( ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 𝑥 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 𝑦 ) ) )
9	3 8	bitr4i	⊢ ( ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) ) ↔ ( 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑥 ∧ 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑦 ) )
10	9	exbii	⊢ ( ∃ 𝑢 ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) ) ↔ ∃ 𝑢 ( 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑥 ∧ 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑦 ) )
11	2 10	bitri	⊢ ( ∃ 𝑢 ∈ 𝐴 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) ↔ ∃ 𝑢 ( 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑥 ∧ 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑦 ) )
12	11	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑥 ∧ 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑦 ) }
13	1 12	eqtr4i	⊢ ≀ ( 𝑅 ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) }