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		ax1w	$⊢ (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))$
5		fr2nr	$⊢ (R Fr A \land (x \in A \land y \in A)) \to \neg (x R y \land y R x)$
6	5	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)$
7		breq2	$⊢ x = z \to (y R x \leftrightarrow y R z)$
8	7	anbi2d	$⊢ x = z \to ((x R y \land y R x) \leftrightarrow (x R y \land y R z))$
9	8	notbid	$⊢ x = z \to (\neg (x R y \land y R x) \leftrightarrow \neg (x R y \land y R z))$
10	6 9	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))$
11		pm2.21	$⊢ \neg (x R y \land y R z) \to ((x R y \land y R z) \to x R z)$
12	10 11	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))$
13		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)$
14		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)$
15	14	biimpri	$⊢ ((x R y \land y R z) \land z R x) \to (x R y \land y R z \land z R x)$
16	15	ancoms	$⊢ (z R x \land (x R y \land y R z)) \to (x R y \land y R z \land z R x)$
17	13 16	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))$
18	17	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)$
19	18	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))$
20	4 12 19	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))$
21		frirr	$⊢ (R Fr A \land x \in A) \to \neg x R x$
22	21	3ad2antr1	$⊢ (R Fr A \land (x \in A \land y \in A \land z \in A)) \to \neg x R x$
23	20 22	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)))$
24	23	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))))$
25	24	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))))$
26	25	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))))$
27	26	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))))$
28		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))$
29		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)))$
30	27 28 29	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)))$
31		breq2	$⊢ y = z \to (x R y \leftrightarrow x R z)$
32		equequ2	$⊢ y = z \to (x = y \leftrightarrow x = z)$
33		breq1	$⊢ y = z \to (y R x \leftrightarrow z R x)$
34	31 32 33	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))$
35	34	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)$
36	34	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)$
37	36	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)$
38	35 37	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)$
39	38	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)$
40		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))$
41	30 39 40	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)$
42	41	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)))$
43	3 42	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))$
44	2 43	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))$
45	44	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))$
46	1 45	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