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

Metamath Proof Explorer

Theorem coss1cnvres

Description: Class of cosets by the converse of a restriction. (Contributed by Peter Mazsa, 8-Jun-2020)

		Ref	Expression
	Assertion	coss1cnvres	⊢ ≀ ^◡ ( 𝑅 ↾ 𝐴 ) = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ∃ 𝑥 ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) ) }

Proof

Step	Hyp	Ref	Expression
1		df-coss	⊢ ≀ ^◡ ( 𝑅 ↾ 𝐴 ) = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ∃ 𝑥 ( 𝑥 ^◡ ( 𝑅 ↾ 𝐴 ) 𝑢 ∧ 𝑥 ^◡ ( 𝑅 ↾ 𝐴 ) 𝑣 ) }
2		br1cnvres	⊢ ( 𝑥 ∈ V → ( 𝑥 ^◡ ( 𝑅 ↾ 𝐴 ) 𝑢 ↔ ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 𝑥 ) ) )
3	2	elv	⊢ ( 𝑥 ^◡ ( 𝑅 ↾ 𝐴 ) 𝑢 ↔ ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 𝑥 ) )
4		br1cnvres	⊢ ( 𝑥 ∈ V → ( 𝑥 ^◡ ( 𝑅 ↾ 𝐴 ) 𝑣 ↔ ( 𝑣 ∈ 𝐴 ∧ 𝑣 𝑅 𝑥 ) ) )
5	4	elv	⊢ ( 𝑥 ^◡ ( 𝑅 ↾ 𝐴 ) 𝑣 ↔ ( 𝑣 ∈ 𝐴 ∧ 𝑣 𝑅 𝑥 ) )
6	3 5	anbi12i	⊢ ( ( 𝑥 ^◡ ( 𝑅 ↾ 𝐴 ) 𝑢 ∧ 𝑥 ^◡ ( 𝑅 ↾ 𝐴 ) 𝑣 ) ↔ ( ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 𝑥 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 𝑅 𝑥 ) ) )
7		an4	⊢ ( ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) ) ↔ ( ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 𝑥 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 𝑅 𝑥 ) ) )
8	6 7	bitr4i	⊢ ( ( 𝑥 ^◡ ( 𝑅 ↾ 𝐴 ) 𝑢 ∧ 𝑥 ^◡ ( 𝑅 ↾ 𝐴 ) 𝑣 ) ↔ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) ) )
9	8	exbii	⊢ ( ∃ 𝑥 ( 𝑥 ^◡ ( 𝑅 ↾ 𝐴 ) 𝑢 ∧ 𝑥 ^◡ ( 𝑅 ↾ 𝐴 ) 𝑣 ) ↔ ∃ 𝑥 ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) ) )
10		19.42v	⊢ ( ∃ 𝑥 ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) ) ↔ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ∃ 𝑥 ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) ) )
11	9 10	bitri	⊢ ( ∃ 𝑥 ( 𝑥 ^◡ ( 𝑅 ↾ 𝐴 ) 𝑢 ∧ 𝑥 ^◡ ( 𝑅 ↾ 𝐴 ) 𝑣 ) ↔ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ∃ 𝑥 ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) ) )
12	11	opabbii	⊢ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ∃ 𝑥 ( 𝑥 ^◡ ( 𝑅 ↾ 𝐴 ) 𝑢 ∧ 𝑥 ^◡ ( 𝑅 ↾ 𝐴 ) 𝑣 ) } = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ∃ 𝑥 ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) ) }
13	1 12	eqtri	⊢ ≀ ^◡ ( 𝑅 ↾ 𝐴 ) = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ∃ 𝑥 ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) ) }