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 ) = ∅ ↔ ∀ 𝑥 ¬ 𝑥 𝑅 𝑥 )