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

Metamath Proof Explorer

Theorem cosscnvssid3

Description: Equivalent expressions for the class of cosets by the converse of R to be a subset of the identity class. (Contributed by Peter Mazsa, 28-Jul-2021)

		Ref	Expression
	Assertion	cosscnvssid3	⊢ ( ≀ ^◡ 𝑅 ⊆ I ↔ ∀ 𝑢 ∀ 𝑣 ∀ 𝑥 ( ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) → 𝑢 = 𝑣 ) )

Proof

Step	Hyp	Ref	Expression
1		cossssid3	⊢ ( ≀ ^◡ 𝑅 ⊆ I ↔ ∀ 𝑥 ∀ 𝑢 ∀ 𝑣 ( ( 𝑥 ^◡ 𝑅 𝑢 ∧ 𝑥 ^◡ 𝑅 𝑣 ) → 𝑢 = 𝑣 ) )
2		alrot3	⊢ ( ∀ 𝑥 ∀ 𝑢 ∀ 𝑣 ( ( 𝑥 ^◡ 𝑅 𝑢 ∧ 𝑥 ^◡ 𝑅 𝑣 ) → 𝑢 = 𝑣 ) ↔ ∀ 𝑢 ∀ 𝑣 ∀ 𝑥 ( ( 𝑥 ^◡ 𝑅 𝑢 ∧ 𝑥 ^◡ 𝑅 𝑣 ) → 𝑢 = 𝑣 ) )
3		brcnvg	⊢ ( ( 𝑥 ∈ V ∧ 𝑢 ∈ V ) → ( 𝑥 ^◡ 𝑅 𝑢 ↔ 𝑢 𝑅 𝑥 ) )
4	3	el2v	⊢ ( 𝑥 ^◡ 𝑅 𝑢 ↔ 𝑢 𝑅 𝑥 )
5		brcnvg	⊢ ( ( 𝑥 ∈ V ∧ 𝑣 ∈ V ) → ( 𝑥 ^◡ 𝑅 𝑣 ↔ 𝑣 𝑅 𝑥 ) )
6	5	el2v	⊢ ( 𝑥 ^◡ 𝑅 𝑣 ↔ 𝑣 𝑅 𝑥 )
7	4 6	anbi12i	⊢ ( ( 𝑥 ^◡ 𝑅 𝑢 ∧ 𝑥 ^◡ 𝑅 𝑣 ) ↔ ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) )
8	7	imbi1i	⊢ ( ( ( 𝑥 ^◡ 𝑅 𝑢 ∧ 𝑥 ^◡ 𝑅 𝑣 ) → 𝑢 = 𝑣 ) ↔ ( ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) → 𝑢 = 𝑣 ) )
9	8	3albii	⊢ ( ∀ 𝑢 ∀ 𝑣 ∀ 𝑥 ( ( 𝑥 ^◡ 𝑅 𝑢 ∧ 𝑥 ^◡ 𝑅 𝑣 ) → 𝑢 = 𝑣 ) ↔ ∀ 𝑢 ∀ 𝑣 ∀ 𝑥 ( ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) → 𝑢 = 𝑣 ) )
10	1 2 9	3bitri	⊢ ( ≀ ^◡ 𝑅 ⊆ I ↔ ∀ 𝑢 ∀ 𝑣 ∀ 𝑥 ( ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) → 𝑢 = 𝑣 ) )