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

Metamath Proof Explorer

Theorem intirr

Description: Two ways of saying a relation is irreflexive. Definition of irreflexivity in Schechter p. 51. (Contributed by NM, 9-Sep-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion intirr ( ( 𝑅 ∩ I ) = ∅ ↔ ∀ 𝑥 ¬ 𝑥 𝑅 𝑥 )

Proof

Step Hyp Ref Expression
1 incom ⊢ ( 𝑅 ∩ I ) = ( I ∩ 𝑅 )
2 1 eqeq1i ⊢ ( ( 𝑅 ∩ I ) = ∅ ↔ ( I ∩ 𝑅 ) = ∅ )
3 disj2 ⊢ ( ( I ∩ 𝑅 ) = ∅ ↔ I ⊆ ( V ∖ 𝑅 ) )
4 reli ⊢ Rel I
5 ssrel ⊢ ( Rel I → ( I ⊆ ( V ∖ 𝑅 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( V ∖ 𝑅 ) ) ) )
6 4 5 ax-mp ⊢ ( I ⊆ ( V ∖ 𝑅 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( V ∖ 𝑅 ) ) )
7 2 3 6 3bitri ⊢ ( ( 𝑅 ∩ I ) = ∅ ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( V ∖ 𝑅 ) ) )
8 equcom ⊢ ( 𝑦 = 𝑥 ↔ 𝑥 = 𝑦 )
9 vex ⊢ 𝑦 ∈ V
10 9 ideq ⊢ ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 )
11 df-br ⊢ ( 𝑥 I 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ I )
12 8 10 11 3bitr2i ⊢ ( 𝑦 = 𝑥 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ I )
13 opex ⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
14 13 biantrur ⊢ ( ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ V ∧ ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) )
15 eldif ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( V ∖ 𝑅 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ V ∧ ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) )
16 14 15 bitr4i ⊢ ( ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( V ∖ 𝑅 ) )
17 df-br ⊢ ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
18 16 17 xchnxbir ⊢ ( ¬ 𝑥 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( V ∖ 𝑅 ) )
19 12 18 imbi12i ⊢ ( ( 𝑦 = 𝑥 → ¬ 𝑥 𝑅 𝑦 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( V ∖ 𝑅 ) ) )
20 19 2albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝑥 → ¬ 𝑥 𝑅 𝑦 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( V ∖ 𝑅 ) ) )
21 breq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑅 𝑥 ) )
22 21 notbid ⊢ ( 𝑦 = 𝑥 → ( ¬ 𝑥 𝑅 𝑦 ↔ ¬ 𝑥 𝑅 𝑥 ) )
23 22 equsalvw ⊢ ( ∀ 𝑦 ( 𝑦 = 𝑥 → ¬ 𝑥 𝑅 𝑦 ) ↔ ¬ 𝑥 𝑅 𝑥 )
24 23 albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝑥 → ¬ 𝑥 𝑅 𝑦 ) ↔ ∀ 𝑥 ¬ 𝑥 𝑅 𝑥 )
25 7 20 24 3bitr2i ⊢ ( ( 𝑅 ∩ I ) = ∅ ↔ ∀ 𝑥 ¬ 𝑥 𝑅 𝑥 )