Theorem cosscnvssid4

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, 31-Aug-2021)

	Ref	Expression
Assertion	cosscnvssid4	⊢ ( ≀ ◡ 𝑅 ⊆ I ↔ ∀ 𝑥 ∃* 𝑢 𝑢 𝑅 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		cossssid4	⊢ ( ≀ ◡ 𝑅 ⊆ I ↔ ∀ 𝑥 ∃* 𝑢 𝑥 ◡ 𝑅 𝑢 )
2		brcnvg	⊢ ( ( 𝑥 ∈ V ∧ 𝑢 ∈ V ) → ( 𝑥 ◡ 𝑅 𝑢 ↔ 𝑢 𝑅 𝑥 ) )
3	2	el2v	⊢ ( 𝑥 ◡ 𝑅 𝑢 ↔ 𝑢 𝑅 𝑥 )
4	3	mobii	⊢ ( ∃* 𝑢 𝑥 ◡ 𝑅 𝑢 ↔ ∃* 𝑢 𝑢 𝑅 𝑥 )
5	4	albii	⊢ ( ∀ 𝑥 ∃* 𝑢 𝑥 ◡ 𝑅 𝑢 ↔ ∀ 𝑥 ∃* 𝑢 𝑢 𝑅 𝑥 )
6	1 5	bitri	⊢ ( ≀ ◡ 𝑅 ⊆ I ↔ ∀ 𝑥 ∃* 𝑢 𝑢 𝑅 𝑥 )