Metamath Proof Explorer


Theorem eldmcoss2

Description: Elementhood in the domain of cosets. (Contributed by Peter Mazsa, 28-Dec-2018)

Ref Expression
Assertion eldmcoss2 ( 𝐴𝑉 → ( 𝐴 ∈ dom ≀ 𝑅𝐴𝑅 𝐴 ) )

Proof

Step Hyp Ref Expression
1 eldmcoss ( 𝐴𝑉 → ( 𝐴 ∈ dom ≀ 𝑅 ↔ ∃ 𝑢 𝑢 𝑅 𝐴 ) )
2 brcoss ( ( 𝐴𝑉𝐴𝑉 ) → ( 𝐴𝑅 𝐴 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐴𝑢 𝑅 𝐴 ) ) )
3 2 anidms ( 𝐴𝑉 → ( 𝐴𝑅 𝐴 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐴𝑢 𝑅 𝐴 ) ) )
4 pm4.24 ( 𝑢 𝑅 𝐴 ↔ ( 𝑢 𝑅 𝐴𝑢 𝑅 𝐴 ) )
5 4 exbii ( ∃ 𝑢 𝑢 𝑅 𝐴 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐴𝑢 𝑅 𝐴 ) )
6 3 5 bitr4di ( 𝐴𝑉 → ( 𝐴𝑅 𝐴 ↔ ∃ 𝑢 𝑢 𝑅 𝐴 ) )
7 1 6 bitr4d ( 𝐴𝑉 → ( 𝐴 ∈ dom ≀ 𝑅𝐴𝑅 𝐴 ) )