Metamath Proof Explorer


Theorem cnvepnep

Description: The membership (epsilon) relation and its converse are disjoint, i.e., _E is an asymmetric relation. Variable-free version of en2lp . (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 19-Jun-2022)

Ref Expression
Assertion cnvepnep ( E ∩ E ) = ∅

Proof

Step Hyp Ref Expression
1 df-eprel E = { ⟨ 𝑦 , 𝑥 ⟩ ∣ 𝑦𝑥 }
2 1 cnveqi E = { ⟨ 𝑦 , 𝑥 ⟩ ∣ 𝑦𝑥 }
3 cnvopab { ⟨ 𝑦 , 𝑥 ⟩ ∣ 𝑦𝑥 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦𝑥 }
4 2 3 eqtri E = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦𝑥 }
5 df-eprel E = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥𝑦 }
6 4 5 ineq12i ( E ∩ E ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦𝑥 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥𝑦 } )
7 inopab ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦𝑥 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥𝑦 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦𝑥𝑥𝑦 ) }
8 6 7 eqtri ( E ∩ E ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦𝑥𝑥𝑦 ) }
9 en2lp ¬ ( 𝑦𝑥𝑥𝑦 )
10 9 gen2 𝑥𝑦 ¬ ( 𝑦𝑥𝑥𝑦 )
11 opab0 ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦𝑥𝑥𝑦 ) } = ∅ ↔ ∀ 𝑥𝑦 ¬ ( 𝑦𝑥𝑥𝑦 ) )
12 10 11 mpbir { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦𝑥𝑥𝑦 ) } = ∅
13 8 12 eqtri ( E ∩ E ) = ∅