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 ⊢ R ∩ I = ∅ ↔ ∀ x ¬ x R x

Proof

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