posn

Description: Partial ordering of a singleton. (Contributed by NM, 27-Apr-2009) (Revised by Mario Carneiro, 23-Apr-2015)

		Ref	Expression
	Assertion	posn	$⊢ Rel R \to (R Po \{A\} \leftrightarrow \neg A R A)$

Proof

Step	Hyp	Ref	Expression
1		po0	$⊢ R Po \emptyset$
2		snprc	$⊢ \neg A \in V \leftrightarrow \{A\} = \emptyset$
3		poeq2	$⊢ \{A\} = \emptyset \to (R Po \{A\} \leftrightarrow R Po \emptyset)$
4	2 3	sylbi	$⊢ \neg A \in V \to (R Po \{A\} \leftrightarrow R Po \emptyset)$
5	1 4	mpbiri	$⊢ \neg A \in V \to R Po \{A\}$
6	5	adantl	$⊢ (Rel R \land \neg A \in V) \to R Po \{A\}$
7		brrelex1	$⊢ (Rel R \land A R A) \to A \in V$
8	7	stoic1a	$⊢ (Rel R \land \neg A \in V) \to \neg A R A$
9	6 8	2thd	$⊢ (Rel R \land \neg A \in V) \to (R Po \{A\} \leftrightarrow \neg A R A)$
10	9	ex	$⊢ Rel R \to (\neg A \in V \to (R Po \{A\} \leftrightarrow \neg A R A))$
11		df-po	$⊢ R Po \{A\} \leftrightarrow \forall x \in \{A\} \forall y \in \{A\} \forall z \in \{A\} (\neg x R x \land ((x R y \land y R z) \to x R z))$
12		breq2	$⊢ z = A \to (y R z \leftrightarrow y R A)$
13	12	anbi2d	$⊢ z = A \to ((x R y \land y R z) \leftrightarrow (x R y \land y R A))$
14		breq2	$⊢ z = A \to (x R z \leftrightarrow x R A)$
15	13 14	imbi12d	$⊢ z = A \to (((x R y \land y R z) \to x R z) \leftrightarrow ((x R y \land y R A) \to x R A))$
16	15	anbi2d	$⊢ z = A \to ((\neg x R x \land ((x R y \land y R z) \to x R z)) \leftrightarrow (\neg x R x \land ((x R y \land y R A) \to x R A)))$
17	16	ralsng	$⊢ A \in V \to (\forall z \in \{A\} (\neg x R x \land ((x R y \land y R z) \to x R z)) \leftrightarrow (\neg x R x \land ((x R y \land y R A) \to x R A)))$
18	17	ralbidv	$⊢ A \in V \to (\forall y \in \{A\} \forall z \in \{A\} (\neg x R x \land ((x R y \land y R z) \to x R z)) \leftrightarrow \forall y \in \{A\} (\neg x R x \land ((x R y \land y R A) \to x R A)))$
19		simpl	$⊢ (x R y \land y R A) \to x R y$
20		breq2	$⊢ y = A \to (x R y \leftrightarrow x R A)$
21	19 20	imbitrid	$⊢ y = A \to ((x R y \land y R A) \to x R A)$
22	21	biantrud	$⊢ y = A \to (\neg x R x \leftrightarrow (\neg x R x \land ((x R y \land y R A) \to x R A)))$
23	22	bicomd	$⊢ y = A \to ((\neg x R x \land ((x R y \land y R A) \to x R A)) \leftrightarrow \neg x R x)$
24	23	ralsng	$⊢ A \in V \to (\forall y \in \{A\} (\neg x R x \land ((x R y \land y R A) \to x R A)) \leftrightarrow \neg x R x)$
25	18 24	bitrd	$⊢ A \in V \to (\forall y \in \{A\} \forall z \in \{A\} (\neg x R x \land ((x R y \land y R z) \to x R z)) \leftrightarrow \neg x R x)$
26	25	ralbidv	$⊢ A \in V \to (\forall x \in \{A\} \forall y \in \{A\} \forall z \in \{A\} (\neg x R x \land ((x R y \land y R z) \to x R z)) \leftrightarrow \forall x \in \{A\} \neg x R x)$
27		breq12	$⊢ (x = A \land x = A) \to (x R x \leftrightarrow A R A)$
28	27	anidms	$⊢ x = A \to (x R x \leftrightarrow A R A)$
29	28	notbid	$⊢ x = A \to (\neg x R x \leftrightarrow \neg A R A)$
30	29	ralsng	$⊢ A \in V \to (\forall x \in \{A\} \neg x R x \leftrightarrow \neg A R A)$
31	26 30	bitrd	$⊢ A \in V \to (\forall x \in \{A\} \forall y \in \{A\} \forall z \in \{A\} (\neg x R x \land ((x R y \land y R z) \to x R z)) \leftrightarrow \neg A R A)$
32	11 31	bitrid	$⊢ A \in V \to (R Po \{A\} \leftrightarrow \neg A R A)$
33	10 32	pm2.61d2	$⊢ Rel R \to (R Po \{A\} \leftrightarrow \neg A R A)$

Metamath Proof Explorer

Theorem posn

Proof