fr3nr

Description: A well-founded relation has no 3-cycle loops. Special case of Proposition 6.23 of TakeutiZaring p. 30. (Contributed by NM, 10-Apr-1994) (Revised by Mario Carneiro, 22-Jun-2015)

		Ref	Expression
	Assertion	fr3nr	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to \neg (B R C \land C R D \land D R B)$

Proof

Step	Hyp	Ref	Expression
1		tpex	$⊢ \{B, C, D\} \in V$
2	1	a1i	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to \{B, C, D\} \in V$
3		simpl	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to R Fr A$
4		df-tp	$⊢ \{B, C, D\} = \{B, C\} \cup \{D\}$
5		simpr1	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to B \in A$
6		simpr2	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to C \in A$
7	5 6	prssd	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to \{B, C\} \subseteq A$
8		simpr3	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to D \in A$
9	8	snssd	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to \{D\} \subseteq A$
10	7 9	unssd	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to \{B, C\} \cup \{D\} \subseteq A$
11	4 10	eqsstrid	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to \{B, C, D\} \subseteq A$
12	5	tpnzd	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to \{B, C, D\} \neq \emptyset$
13		fri	$⊢ ((\{B, C, D\} \in V \land R Fr A) \land (\{B, C, D\} \subseteq A \land \{B, C, D\} \neq \emptyset)) \to \exists x \in \{B, C, D\} \forall y \in \{B, C, D\} \neg y R x$
14	2 3 11 12 13	syl22anc	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to \exists x \in \{B, C, D\} \forall y \in \{B, C, D\} \neg y R x$
15		breq2	$⊢ x = B \to (y R x \leftrightarrow y R B)$
16	15	notbid	$⊢ x = B \to (\neg y R x \leftrightarrow \neg y R B)$
17	16	ralbidv	$⊢ x = B \to (\forall y \in \{B, C, D\} \neg y R x \leftrightarrow \forall y \in \{B, C, D\} \neg y R B)$
18		breq2	$⊢ x = C \to (y R x \leftrightarrow y R C)$
19	18	notbid	$⊢ x = C \to (\neg y R x \leftrightarrow \neg y R C)$
20	19	ralbidv	$⊢ x = C \to (\forall y \in \{B, C, D\} \neg y R x \leftrightarrow \forall y \in \{B, C, D\} \neg y R C)$
21		breq2	$⊢ x = D \to (y R x \leftrightarrow y R D)$
22	21	notbid	$⊢ x = D \to (\neg y R x \leftrightarrow \neg y R D)$
23	22	ralbidv	$⊢ x = D \to (\forall y \in \{B, C, D\} \neg y R x \leftrightarrow \forall y \in \{B, C, D\} \neg y R D)$
24	17 20 23	rextpg	$⊢ (B \in A \land C \in A \land D \in A) \to (\exists x \in \{B, C, D\} \forall y \in \{B, C, D\} \neg y R x \leftrightarrow (\forall y \in \{B, C, D\} \neg y R B \lor \forall y \in \{B, C, D\} \neg y R C \lor \forall y \in \{B, C, D\} \neg y R D))$
25	24	adantl	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to (\exists x \in \{B, C, D\} \forall y \in \{B, C, D\} \neg y R x \leftrightarrow (\forall y \in \{B, C, D\} \neg y R B \lor \forall y \in \{B, C, D\} \neg y R C \lor \forall y \in \{B, C, D\} \neg y R D))$
26	14 25	mpbid	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to (\forall y \in \{B, C, D\} \neg y R B \lor \forall y \in \{B, C, D\} \neg y R C \lor \forall y \in \{B, C, D\} \neg y R D)$
27		snsstp3	$⊢ \{D\} \subseteq \{B, C, D\}$
28		snssg	$⊢ D \in A \to (D \in \{B, C, D\} \leftrightarrow \{D\} \subseteq \{B, C, D\})$
29	8 28	syl	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to (D \in \{B, C, D\} \leftrightarrow \{D\} \subseteq \{B, C, D\})$
30	27 29	mpbiri	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to D \in \{B, C, D\}$
31		breq1	$⊢ y = D \to (y R B \leftrightarrow D R B)$
32	31	notbid	$⊢ y = D \to (\neg y R B \leftrightarrow \neg D R B)$
33	32	rspcv	$⊢ D \in \{B, C, D\} \to (\forall y \in \{B, C, D\} \neg y R B \to \neg D R B)$
34	30 33	syl	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to (\forall y \in \{B, C, D\} \neg y R B \to \neg D R B)$
35		snsstp1	$⊢ \{B\} \subseteq \{B, C, D\}$
36		snssg	$⊢ B \in A \to (B \in \{B, C, D\} \leftrightarrow \{B\} \subseteq \{B, C, D\})$
37	5 36	syl	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to (B \in \{B, C, D\} \leftrightarrow \{B\} \subseteq \{B, C, D\})$
38	35 37	mpbiri	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to B \in \{B, C, D\}$
39		breq1	$⊢ y = B \to (y R C \leftrightarrow B R C)$
40	39	notbid	$⊢ y = B \to (\neg y R C \leftrightarrow \neg B R C)$
41	40	rspcv	$⊢ B \in \{B, C, D\} \to (\forall y \in \{B, C, D\} \neg y R C \to \neg B R C)$
42	38 41	syl	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to (\forall y \in \{B, C, D\} \neg y R C \to \neg B R C)$
43		snsstp2	$⊢ \{C\} \subseteq \{B, C, D\}$
44		snssg	$⊢ C \in A \to (C \in \{B, C, D\} \leftrightarrow \{C\} \subseteq \{B, C, D\})$
45	6 44	syl	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to (C \in \{B, C, D\} \leftrightarrow \{C\} \subseteq \{B, C, D\})$
46	43 45	mpbiri	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to C \in \{B, C, D\}$
47		breq1	$⊢ y = C \to (y R D \leftrightarrow C R D)$
48	47	notbid	$⊢ y = C \to (\neg y R D \leftrightarrow \neg C R D)$
49	48	rspcv	$⊢ C \in \{B, C, D\} \to (\forall y \in \{B, C, D\} \neg y R D \to \neg C R D)$
50	46 49	syl	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to (\forall y \in \{B, C, D\} \neg y R D \to \neg C R D)$
51	34 42 50	3orim123d	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to ((\forall y \in \{B, C, D\} \neg y R B \lor \forall y \in \{B, C, D\} \neg y R C \lor \forall y \in \{B, C, D\} \neg y R D) \to (\neg D R B \lor \neg B R C \lor \neg C R D))$
52	26 51	mpd	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to (\neg D R B \lor \neg B R C \lor \neg C R D)$
53		3ianor	$⊢ \neg (D R B \land B R C \land C R D) \leftrightarrow (\neg D R B \lor \neg B R C \lor \neg C R D)$
54	52 53	sylibr	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to \neg (D R B \land B R C \land C R D)$
55		3anrot	$⊢ (D R B \land B R C \land C R D) \leftrightarrow (B R C \land C R D \land D R B)$
56	54 55	sylnib	$⊢ (R Fr A \land (B \in A \land C \in A \land D \in A)) \to \neg (B R C \land C R D \land D R B)$

Metamath Proof Explorer

Theorem fr3nr

Proof