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 ↔ ∀ 𝑢𝑣𝑥 ( ( 𝑢 𝑅 𝑥𝑣 𝑅 𝑥 ) → 𝑢 = 𝑣 ) )