dfwe2

Description: Alternate definition of well-ordering. Definition 6.24(2) of TakeutiZaring p. 30. (Contributed by NM, 16-Mar-1997) (Proof shortened by Andrew Salmon, 12-Aug-2011)

		Ref	Expression
	Assertion	dfwe2	$⊢ R We A \leftrightarrow (R Fr A \land \forall x \in A \forall y \in A (x R y \lor x = y \lor y R x))$

Proof

Step	Hyp	Ref	Expression
1		df-we	$⊢ R We A \leftrightarrow (R Fr A \land R Or A)$
2		df-so	$⊢ R Or A \leftrightarrow (R Po A \land \forall x \in A \forall y \in A (x R y \lor x = y \lor y R x))$
3		simpr	$⊢ (R Po A \land \forall x \in A \forall y \in A (x R y \lor x = y \lor y R x)) \to \forall x \in A \forall y \in A (x R y \lor x = y \lor y R x)$
4		ax-1	$⊢ x R z \to ((x R y \land y R z) \to x R z)$
5	4	a1i	$⊢ (R Fr A \land (x \in A \land y \in A \land z \in A)) \to (x R z \to ((x R y \land y R z) \to x R z))$
6		fr2nr	$⊢ (R Fr A \land (x \in A \land y \in A)) \to \neg (x R y \land y R x)$
7	6	3adantr3	$⊢ (R Fr A \land (x \in A \land y \in A \land z \in A)) \to \neg (x R y \land y R x)$
8		breq2	$⊢ x = z \to (y R x \leftrightarrow y R z)$
9	8	anbi2d	$⊢ x = z \to ((x R y \land y R x) \leftrightarrow (x R y \land y R z))$
10	9	notbid	$⊢ x = z \to (\neg (x R y \land y R x) \leftrightarrow \neg (x R y \land y R z))$
11	7 10	syl5ibcom	$⊢ (R Fr A \land (x \in A \land y \in A \land z \in A)) \to (x = z \to \neg (x R y \land y R z))$
12		pm2.21	$⊢ \neg (x R y \land y R z) \to ((x R y \land y R z) \to x R z)$
13	11 12	syl6	$⊢ (R Fr A \land (x \in A \land y \in A \land z \in A)) \to (x = z \to ((x R y \land y R z) \to x R z))$
14		fr3nr	$⊢ (R Fr A \land (x \in A \land y \in A \land z \in A)) \to \neg (x R y \land y R z \land z R x)$
15		df-3an	$⊢ (x R y \land y R z \land z R x) \leftrightarrow ((x R y \land y R z) \land z R x)$
16	15	biimpri	$⊢ ((x R y \land y R z) \land z R x) \to (x R y \land y R z \land z R x)$
17	16	ancoms	$⊢ (z R x \land (x R y \land y R z)) \to (x R y \land y R z \land z R x)$
18	14 17	nsyl	$⊢ (R Fr A \land (x \in A \land y \in A \land z \in A)) \to \neg (z R x \land (x R y \land y R z))$
19	18	pm2.21d	$⊢ (R Fr A \land (x \in A \land y \in A \land z \in A)) \to ((z R x \land (x R y \land y R z)) \to x R z)$
20	19	expd	$⊢ (R Fr A \land (x \in A \land y \in A \land z \in A)) \to (z R x \to ((x R y \land y R z) \to x R z))$
21	5 13 20	3jaod	$⊢ (R Fr A \land (x \in A \land y \in A \land z \in A)) \to ((x R z \lor x = z \lor z R x) \to ((x R y \land y R z) \to x R z))$
22		frirr	$⊢ (R Fr A \land x \in A) \to \neg x R x$
23	22	3ad2antr1	$⊢ (R Fr A \land (x \in A \land y \in A \land z \in A)) \to \neg x R x$
24	21 23	jctild	$⊢ (R Fr A \land (x \in A \land y \in A \land z \in A)) \to ((x R z \lor x = z \lor z R x) \to (\neg x R x \land ((x R y \land y R z) \to x R z)))$
25	24	ex	$⊢ R Fr A \to ((x \in A \land y \in A \land z \in A) \to ((x R z \lor x = z \lor z R x) \to (\neg x R x \land ((x R y \land y R z) \to x R z))))$
26	25	a2d	$⊢ R Fr A \to (((x \in A \land y \in A \land z \in A) \to (x R z \lor x = z \lor z R x)) \to ((x \in A \land y \in A \land z \in A) \to (\neg x R x \land ((x R y \land y R z) \to x R z))))$
27	26	alimdv	$⊢ R Fr A \to (\forall z ((x \in A \land y \in A \land z \in A) \to (x R z \lor x = z \lor z R x)) \to \forall z ((x \in A \land y \in A \land z \in A) \to (\neg x R x \land ((x R y \land y R z) \to x R z))))$
28	27	2alimdv	$⊢ R Fr A \to (\forall x \forall y \forall z ((x \in A \land y \in A \land z \in A) \to (x R z \lor x = z \lor z R x)) \to \forall x \forall y \forall z ((x \in A \land y \in A \land z \in A) \to (\neg x R x \land ((x R y \land y R z) \to x R z))))$
29		r3al	$⊢ \forall x \in A \forall y \in A \forall z \in A (x R z \lor x = z \lor z R x) \leftrightarrow \forall x \forall y \forall z ((x \in A \land y \in A \land z \in A) \to (x R z \lor x = z \lor z R x))$
30		r3al	$⊢ \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 \forall y \forall z ((x \in A \land y \in A \land z \in A) \to (\neg x R x \land ((x R y \land y R z) \to x R z)))$
31	28 29 30	3imtr4g	$⊢ R Fr A \to (\forall x \in A \forall y \in A \forall z \in A (x R z \lor x = z \lor z R x) \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)))$
32		breq2	$⊢ y = z \to (x R y \leftrightarrow x R z)$
33		equequ2	$⊢ y = z \to (x = y \leftrightarrow x = z)$
34		breq1	$⊢ y = z \to (y R x \leftrightarrow z R x)$
35	32 33 34	3orbi123d	$⊢ y = z \to ((x R y \lor x = y \lor y R x) \leftrightarrow (x R z \lor x = z \lor z R x))$
36	35	ralidmw	$⊢ \forall y \in A \forall y \in A (x R y \lor x = y \lor y R x) \leftrightarrow \forall y \in A (x R y \lor x = y \lor y R x)$
37	35	cbvralvw	$⊢ \forall y \in A (x R y \lor x = y \lor y R x) \leftrightarrow \forall z \in A (x R z \lor x = z \lor z R x)$
38	37	ralbii	$⊢ \forall y \in A \forall y \in A (x R y \lor x = y \lor y R x) \leftrightarrow \forall y \in A \forall z \in A (x R z \lor x = z \lor z R x)$
39	36 38	bitr3i	$⊢ \forall y \in A (x R y \lor x = y \lor y R x) \leftrightarrow \forall y \in A \forall z \in A (x R z \lor x = z \lor z R x)$
40	39	ralbii	$⊢ \forall x \in A \forall y \in A (x R y \lor x = y \lor y R x) \leftrightarrow \forall x \in A \forall y \in A \forall z \in A (x R z \lor x = z \lor z R x)$
41		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))$
42	31 40 41	3imtr4g	$⊢ R Fr A \to (\forall x \in A \forall y \in A (x R y \lor x = y \lor y R x) \to R Po A)$
43	42	ancrd	$⊢ R Fr A \to (\forall x \in A \forall y \in A (x R y \lor x = y \lor y R x) \to (R Po A \land \forall x \in A \forall y \in A (x R y \lor x = y \lor y R x)))$
44	3 43	impbid2	$⊢ R Fr A \to ((R Po A \land \forall x \in A \forall y \in A (x R y \lor x = y \lor y R x)) \leftrightarrow \forall x \in A \forall y \in A (x R y \lor x = y \lor y R x))$
45	2 44	bitrid	$⊢ R Fr A \to (R Or A \leftrightarrow \forall x \in A \forall y \in A (x R y \lor x = y \lor y R x))$
46	45	pm5.32i	$⊢ (R Fr A \land R Or A) \leftrightarrow (R Fr A \land \forall x \in A \forall y \in A (x R y \lor x = y \lor y R x))$
47	1 46	bitri	$⊢ R We A \leftrightarrow (R Fr A \land \forall x \in A \forall y \in A (x R y \lor x = y \lor y R x))$

Metamath Proof Explorer

Theorem dfwe2

Proof