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

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 ) = ∅