poirr2

Description: A partial order is irreflexive. (Contributed by Mario Carneiro, 2-Nov-2015) (Proof shortened by Peter Mazsa, 2-Oct-2022)

		Ref	Expression
	Assertion	poirr2	$⊢ R Po A \to R \cap ({I ↾}_{A}) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		relres	$⊢ Rel ({I ↾}_{A})$
2		relin2	$⊢ Rel ({I ↾}_{A}) \to Rel (R \cap ({I ↾}_{A}))$
3	1 2	mp1i	$⊢ R Po A \to Rel (R \cap ({I ↾}_{A}))$
4		df-br	$⊢ x (R \cap ({I ↾}_{A})) y \leftrightarrow ⟨x, y⟩ \in (R \cap ({I ↾}_{A}))$
5		brin	$⊢ x (R \cap ({I ↾}_{A})) y \leftrightarrow (x R y \land x ({I ↾}_{A}) y)$
6	4 5	bitr3i	$⊢ ⟨x, y⟩ \in (R \cap ({I ↾}_{A})) \leftrightarrow (x R y \land x ({I ↾}_{A}) y)$
7		vex	$⊢ y \in V$
8	7	brresi	$⊢ x ({I ↾}_{A}) y \leftrightarrow (x \in A \land x I y)$
9		poirr	$⊢ (R Po A \land x \in A) \to \neg x R x$
10	7	ideq	$⊢ x I y \leftrightarrow x = y$
11		breq2	$⊢ x = y \to (x R x \leftrightarrow x R y)$
12	10 11	sylbi	$⊢ x I y \to (x R x \leftrightarrow x R y)$
13	12	notbid	$⊢ x I y \to (\neg x R x \leftrightarrow \neg x R y)$
14	9 13	syl5ibcom	$⊢ (R Po A \land x \in A) \to (x I y \to \neg x R y)$
15	14	expimpd	$⊢ R Po A \to ((x \in A \land x I y) \to \neg x R y)$
16	8 15	biimtrid	$⊢ R Po A \to (x ({I ↾}_{A}) y \to \neg x R y)$
17	16	con2d	$⊢ R Po A \to (x R y \to \neg x ({I ↾}_{A}) y)$
18		imnan	$⊢ (x R y \to \neg x ({I ↾}_{A}) y) \leftrightarrow \neg (x R y \land x ({I ↾}_{A}) y)$
19	17 18	sylib	$⊢ R Po A \to \neg (x R y \land x ({I ↾}_{A}) y)$
20	19	pm2.21d	$⊢ R Po A \to ((x R y \land x ({I ↾}_{A}) y) \to ⟨x, y⟩ \in \emptyset)$
21	6 20	biimtrid	$⊢ R Po A \to (⟨x, y⟩ \in (R \cap ({I ↾}_{A})) \to ⟨x, y⟩ \in \emptyset)$
22	3 21	relssdv	$⊢ R Po A \to R \cap ({I ↾}_{A}) \subseteq \emptyset$
23		ss0	$⊢ R \cap ({I ↾}_{A}) \subseteq \emptyset \to R \cap ({I ↾}_{A}) = \emptyset$
24	22 23	syl	$⊢ R Po A \to R \cap ({I ↾}_{A}) = \emptyset$

Metamath Proof Explorer

Theorem poirr2

Proof