frsn

Description: Founded relation on a singleton. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by Mario Carneiro, 23-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		snprc	$⊢ \neg A \in V \leftrightarrow \{A\} = \emptyset$
2		fr0	$⊢ R Fr \emptyset$
3		freq2	$⊢ \{A\} = \emptyset \to (R Fr \{A\} \leftrightarrow R Fr \emptyset)$
4	2 3	mpbiri	$⊢ \{A\} = \emptyset \to R Fr \{A\}$
5	1 4	sylbi	$⊢ \neg A \in V \to R Fr \{A\}$
6	5	adantl	$⊢ (Rel R \land \neg A \in V) \to R Fr \{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 Fr \{A\} \leftrightarrow \neg A R A)$
10	9	ex	$⊢ Rel R \to (\neg A \in V \to (R Fr \{A\} \leftrightarrow \neg A R A))$
11		df-fr	$⊢ R Fr \{A\} \leftrightarrow \forall x ((x \subseteq \{A\} \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z R y)$
12		sssn	$⊢ x \subseteq \{A\} \leftrightarrow (x = \emptyset \lor x = \{A\})$
13		neor	$⊢ (x = \emptyset \lor x = \{A\}) \leftrightarrow (x \neq \emptyset \to x = \{A\})$
14	12 13	sylbb	$⊢ x \subseteq \{A\} \to (x \neq \emptyset \to x = \{A\})$
15	14	imp	$⊢ (x \subseteq \{A\} \land x \neq \emptyset) \to x = \{A\}$
16	15	adantl	$⊢ (A \in V \land (x \subseteq \{A\} \land x \neq \emptyset)) \to x = \{A\}$
17		eqimss	$⊢ x = \{A\} \to x \subseteq \{A\}$
18	17	adantl	$⊢ (A \in V \land x = \{A\}) \to x \subseteq \{A\}$
19		snnzg	$⊢ A \in V \to \{A\} \neq \emptyset$
20		neeq1	$⊢ x = \{A\} \to (x \neq \emptyset \leftrightarrow \{A\} \neq \emptyset)$
21	19 20	syl5ibrcom	$⊢ A \in V \to (x = \{A\} \to x \neq \emptyset)$
22	21	imp	$⊢ (A \in V \land x = \{A\}) \to x \neq \emptyset$
23	18 22	jca	$⊢ (A \in V \land x = \{A\}) \to (x \subseteq \{A\} \land x \neq \emptyset)$
24	16 23	impbida	$⊢ A \in V \to ((x \subseteq \{A\} \land x \neq \emptyset) \leftrightarrow x = \{A\})$
25	24	imbi1d	$⊢ A \in V \to (((x \subseteq \{A\} \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z R y) \leftrightarrow (x = \{A\} \to \exists y \in x \forall z \in x \neg z R y))$
26	25	albidv	$⊢ A \in V \to (\forall x ((x \subseteq \{A\} \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z R y) \leftrightarrow \forall x (x = \{A\} \to \exists y \in x \forall z \in x \neg z R y))$
27		snex	$⊢ \{A\} \in V$
28		raleq	$⊢ x = \{A\} \to (\forall z \in x \neg z R y \leftrightarrow \forall z \in \{A\} \neg z R y)$
29	28	rexeqbi1dv	$⊢ x = \{A\} \to (\exists y \in x \forall z \in x \neg z R y \leftrightarrow \exists y \in \{A\} \forall z \in \{A\} \neg z R y)$
30	27 29	ceqsalv	$⊢ \forall x (x = \{A\} \to \exists y \in x \forall z \in x \neg z R y) \leftrightarrow \exists y \in \{A\} \forall z \in \{A\} \neg z R y$
31	26 30	bitrdi	$⊢ A \in V \to (\forall x ((x \subseteq \{A\} \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z R y) \leftrightarrow \exists y \in \{A\} \forall z \in \{A\} \neg z R y)$
32	11 31	bitrid	$⊢ A \in V \to (R Fr \{A\} \leftrightarrow \exists y \in \{A\} \forall z \in \{A\} \neg z R y)$
33		breq2	$⊢ y = A \to (z R y \leftrightarrow z R A)$
34	33	notbid	$⊢ y = A \to (\neg z R y \leftrightarrow \neg z R A)$
35	34	ralbidv	$⊢ y = A \to (\forall z \in \{A\} \neg z R y \leftrightarrow \forall z \in \{A\} \neg z R A)$
36	35	rexsng	$⊢ A \in V \to (\exists y \in \{A\} \forall z \in \{A\} \neg z R y \leftrightarrow \forall z \in \{A\} \neg z R A)$
37		breq1	$⊢ z = A \to (z R A \leftrightarrow A R A)$
38	37	notbid	$⊢ z = A \to (\neg z R A \leftrightarrow \neg A R A)$
39	38	ralsng	$⊢ A \in V \to (\forall z \in \{A\} \neg z R A \leftrightarrow \neg A R A)$
40	32 36 39	3bitrd	$⊢ A \in V \to (R Fr \{A\} \leftrightarrow \neg A R A)$
41	10 40	pm2.61d2	$⊢ Rel R \to (R Fr \{A\} \leftrightarrow \neg A R A)$

Metamath Proof Explorer

Theorem frsn

Proof