Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem dfwe2 2187

Description: Alternate definition of well-ordering. Definition 6.24(2) of [TakeutiZaring] p. 30.

**Assertion**
Ref	Expression
dfwe2	⊢ (R We A ↔ (R Fr A ∧ ∀x ∈ A ∀y ∈ A (xRy ∨ x = y ∨ yRx)))

Distinct variable group(s): x,y,R x,A,y

**Proof of Theorem dfwe2**
Step	Hyp	Ref	Expression
1		df-we 2186	. 2 ⊢ (R We A ↔ (R Fr A ∧ R Or A))
2		solin 2145	. . . . . . 7 ⊢ ((R Or A ∧ (x ∈ A ∧ y ∈ A)) → (xRy ∨ x = y ∨ yRx))
3	2	exp 291	. . . . . 6 ⊢ (R Or A → ((x ∈ A ∧ y ∈ A) → (xRy ∨ x = y ∨ yRx)))
4	3	19.21aivv 944	. . . . 5 ⊢ (R Or A → ∀x∀y((x ∈ A ∧ y ∈ A) → (xRy ∨ x = y ∨ yRx)))
5		r2al 1231	. . . . 5 ⊢ (∀x ∈ A ∀y ∈ A (xRy ∨ x = y ∨ yRx) ↔ ∀x∀y>(x ∈ A ∧ y ∈ A) → (xRy ∨ x = y ∨ yRx)))
6	4, 5	sylibr 175	. . . 4 ⊢ (R Or A → ∀x ∈ A ∀y ∈ A (xRy ∨ x = y ∨ yRx))
7	6	anim2i 270	. . 3 ⊢ ((R Fr A ∧ R Or A) → (R Fr A ∧ ∀x ∈ A ∀y ∈ A (xRy ∨ x = y ∨ yRx)))
8		frirr 2176	. . . . . . . . . . . . . . . . 17 ⊢ ((R Fr A ∧ x ∈ A) → ¬ xRx)
9	8	adantrr 312	. . . . . . . . . . . . . . . 16 ⊢ ((R Fr A ∧ (x ∈ A ∧ y ∈ A)) → ¬ xRx)
10		3simpa 591	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ A ∧ y ∈ A ∧ z ∈ A) → (x ∈ A ∧ y ∈ A))
11	9, 10	sylan2 346	. . . . . . . . . . . . . . 15 ⊢ ((R Fr A ∧ (x ∈ A ∧ y ∈ A ∧ z ∈ A)) → ¬ xRx)
12	11	a1d 14	. . . . . . . . . . . . . 14 ⊢ ((R Fr A ∧ (x ∈ A ∧ y ∈ A ∧ z ∈ A)) → ((xRz ∨ x = z ∨ zRx) → ¬ xRx))
13		fr2nr 2177	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((R Fr A ∧ (x ∈ A ∧ y ∈ A)) → ¬ (xRy ∧ yRx))
14	13, 10	sylan2 346	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((R Fr A ∧ (x ∈ A ∧ y ∈ A ∧ z ∈ A)) → ¬ (xRy ∧ yRx))
15		breq2 2066	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (x = z → (yRx ↔ yRz))
16	15	biimprd 136	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (x = z → (yRz → yRx))
17	16	anim2d 433	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (x = z → ((xRy ∧ yRz) → (xRy ∧ yRx)))
18	17	com12 13	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((xRy ∧ yRz) → (x = z → (xRy ∧ yRx)))
19	18	imp 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((xRy ∧ yRz) ∧ x = z) → (xRy ∧ yRx))
20	14, 19	nsyl 102	. . . . . . . . . . . . . . . . . . 19 ⊢ ((R Fr A ∧ (x ∈ A ∧ y ∈ A ∧ z ∈ A)) → ¬ ((xRy ∧ yRz) ∧ x = z))
21		imnan 207	. . . . . . . . . . . . . . . . . . 19 ⊢ (((xRy ∧ yRz) → ¬ x = z) ↔ ¬ ((xRy ∧ yRz) ∧ x = z))
22	20, 21	sylibr 175	. . . . . . . . . . . . . . . . . 18 ⊢ ((R Fr A ∧ (x ∈ A ∧ y ∈ A ∧ z ∈ A)) → ((xRy ∧ yRz) → ¬ x = z))
23		fr3nr 2178	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((R Fr A ∧ (x ∈ A ∧ y ∈ A ∧ z ∈ A)) → ¬ (xRy ∧ yRz ∧ zRx))
24		df-3an 583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((xRy ∧ yRz ∧ zRx) ↔ ((xRy ∧ yRz) ∧ zRx))
25	24	negbii 162	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (xRy ∧ yRz ∧ zRx) ↔ ¬ ((xRy ∧ yRz) ∧ zRx))
26	23, 25	sylib 173	. . . . . . . . . . . . . . . . . . 19 ⊢ ((R Fr A ∧ (x ∈ A ∧ y ∈ A ∧ z ∈ A)) → ¬ ((xRy ∧ yRz) ∧ zRx))
27		imnan 207	. . . . . . . . . . . . . . . . . . 19 ⊢ (((xRy ∧ yRz) → ¬ zRx) ↔ ¬ ((xRy ∧ yRz) ∧ zRx))
28	26, 27	sylibr 175	. . . . . . . . . . . . . . . . . 18 ⊢ ((R Fr A ∧ (x ∈ A ∧ y ∈ A ∧ z ∈ A)) → ((xRy ∧ yRz) → ¬ zRx))
29	22, 28	jcad 455	. . . . . . . . . . . . . . . . 17 ⊢ ((R Fr A ∧ (x ∈ A ∧ y ∈ A ∧ z ∈ A)) → ((xRy ∧ yRz) → (¬ x = z ∧ ¬ zRx)))
30		ioran 254	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (x = z ∨ zRx) ↔ (¬ x = z ∧ ¬ zRx))
31	29, 30	syl6ibr 186	. . . . . . . . . . . . . . . 16 ⊢ ((R Fr A ∧ (x ∈ A ∧ y ∈ A ∧ z ∈ A)) → ((xRy ∧ yRz) → ¬ (x = z ∨ zRx)))
32	31	syl4d 28	. . . . . . . . . . . . . . 15 ⊢ ((R Fr A ∧ (x ∈ A ∧ y ∈ A ∧ z ∈ A)) → ((¬ (x = z ∨ zRx) → xRz) → ((xRy ∧ yRz) → xRz)))
33		3orass 584	. . . . . . . . . . . . . . . 16 ⊢ ((xRz ∨ x = z ∨ zRx) ↔ (xRz ∨ (x = z ∨ zRx)))
34		orcom 209	. . . . . . . . . . . . . . . 16 ⊢ ((xRz ∨ ( = z ∨ zRx)) ↔ ((x = z ∨ zRx) ∨ xRz))
35		df-or 197	. . . . . . . . . . . . . . . 16 ⊢ (((x = z ∨ zRx) ∨ xRz) ↔ (¬ (x = z ∨ zRx) → xRz))
36	33, 34, 35	3bitr 155	. . . . . . . . . . . . . . 15 ⊢ ((xRz ∨ x = z ∨ zRx) ↔ (¬ (x = z ∨ zRx) → xRz))
37	32, 36	syl5ib 181	. . . . . . . . . . . . . 14 ⊢ ((R Fr A ∧ (x ∈ A ∧ y ∈ A ∧ z ∈ A)) → ((xRz ∨ x = z ∨ zRx) → ((xRy ∧ yRz) → xRz)))
38	12, 37	jcad 455	. . . . . . . . . . . . 13 ⊢ ((R Fr ∧ (x ∈ A ∧ y ∈ A ∧ z ∈ A)) → ((xRz ∨ x = z ∨ zRx) → (¬ xRx ∧ ((xRy ∧ yRz) → xRz))))
39	38	exp 291	. . . . . . . . . . . 12 ⊢ (R Fr A → ((x ∈ A ∧ y ∈ A ∧ z ∈ A) → ((xRz ∨ x = z ∨ zRx) → (¬ xRx ∧ ((xRy ∧ yRz) → xRz)))))
40	39	a2d 15	. . . . . . . . . . 11 ⊢ (R Fr A → (((x ∈ A ∧ y ∈ A ∧ z ∈ A) → (xRz ∨ x = z ∨ zRx)) → ((x ∈ A ∧ y ∈ A ∧ z ∈ A) → (¬ xRx ∧ ((xRy ∧ yRz) → xRz)))))
41	40	19.20dv 946	. . . . . . . . . 10 ⊢ (R Fr A → (∀z((x ∈ A ∧ y ∈ A ∧ z ∈ A) → (xRz ∨ x = z ∨ zRx)) → ∀z((x ∈ A ∧ y ∈ A ∧ z ∈ A) → (¬ xRx ∧ ((xRy ∧ yRz) → xRz)))))
42	41	19.20dv 946	. . . . . . . . 9 ⊢ (R Fr A → (∀y∀z((x ∈ A ∧ y ∈ A ∧ z ∈ A) → (xRz ∨ x = z ∨ zRx)) → ∀y∀z((x ∈ A ∧ y ∈ A ∧ z ∈ A) → (¬ xRx ∧ ((xRy ∧ yRz) → xRz)))))
43	42	19.20dv 946	. . . . . . . 8 ⊢ (R Fr A → (∀x∀y∀z((x ∈ A ∧ y ∈ A ∧ z ∈ A) → (xRz ∨ x = z ∨ zRx)) → ∀x∀y∀z((x ∈ A ∧ y ∈ A ∧ z ∈ A) → (¬ xRx ∧ ((xRy ∧ yRz) → xRz)))))
44		r3al 1240	. . . . . . . 8 ⊢ (∀x ∈ A ∀y ∈ A ∀z ∈ A (xRz ∨ x = z ∨ zRx) ↔ ∀x∀y∀z((x ∈ A ∧ y ∈ A ∧ z ∈ A) → (xRz ∨ x = z ∨ zRx)))
45		r3al 1240	. . . . . . . 8 ⊢ (∀x ∈ A ∀y ∈ A ∀z ∈ A (¬ xRx ∧ ((xRy ∧ yRz) → xRz)) ↔ ∀x∀y∀z((x ∈ A ∧ y ∈ A ∧ z ∈ A) → (¬ xRx ∧ ((xRy ∧ yRz) → xRz))))
46	43, 44, 45	3imtr4g 426	. . . . . . 7 ⊢ (R Fr A → (∀x ∈ A ∀y ∈ A ∀z ∈ A (xRz ∨ x = z ∨ zRx) → ∀x ∈ A ∀y ∈ A ∀z ∈ A (¬ xRx ∧ ((xRy ∧ yRz) → xRz))))
47		ralidm 1774	. . . . . . . . 9 ⊢ (∀y ∈ A ∀y ∈ A (xRy ∨ x = y ∨ yRx) ↔ ∀y ∈ A (xRy ∨ x = y ∨ yRx))
48		breq2 2066	. . . . . . . . . . . 12 ⊢ (y = z → (xRy ↔ xRz))
49		cleq2 1110	. . . . . . . . . . . 12 ⊢ (y = z → (x = y ↔ x = z))
50		breq1 2065	. . . . . . . . . . . 12 ⊢ (y = z → (yRx ↔ zRx))
51	48, 49, 50	bi3ord 635	. . . . . . . . . . 11 ⊢ (y = z → ((xRy ∨ x = y ∨ yRx) ↔ (xRz ∨ x = z ∨ zRx)))
52	51	cbvralv 1333	. . . . . . . . . 10 ⊢ (∀y ∈ A (xRy ∨ x = y ∨ yRx) ↔ ∀z ∈ A (xRz ∨ x = z ∨ zRx))
53	52	biral 1223	. . . . . . . . 9 ⊢ (∀y ∈ A ∀y ∈ A (xRy ∨ x = y ∨ yRx) ↔ ∀y ∈ A ∀z ∈ A (xRz ∨ x = z ∨ zRx))
54	47, 53	bitr3 153	. . . . . . . 8 ⊢ (∀y ∈ A (xRy ∨ x = y ∨ yRx) ↔ ∀y ∈ A ∀z ∈ A (xRz ∨ x = z ∨ zRx))
55	54	biral 1223	. . . . . . 7 ⊢ (∀x ∈ A ∀y ∈ A (xRy ∨ x = y ∨ yRx) ↔ ∀x ∈ A ∀y ∈ A ∀z ∈ A (xRz ∨ x = z ∨ zRx))
56		df-po 2128	. . . . . . 7 ⊢ (R Po A ↔ ∀x ∈ A ∀y ∈ A ∀z ∈ A (¬ xRx ∧ ((xRy ∧ yRz) → xRz)))
57	46, 55, 56	3imtr4g 426	. . . . . 6 ⊢ (R Fr A → (∀x ∈ A ∀y ∈ A (xRy ∨ x = y ∨ yRx) → R Po A))
58	57	ancrd 247	. . . . 5 ⊢ (R Fr A → (∀x ∈ A ∀y ∈ A (xRy ∨ x = y ∨ yRx) → (R Po A ∧ ∀x ∈ A ∀y ∈ A (xRy ∨ x = y ∨ yRx))))
59		df-so 2138	. . . . 5 ⊢ (R Or A ↔ (R Po A ∧ ∀x ∈ A ∀y ∈ A (xRy ∨ x = y ∨ yRx)))
60	58, 59	syl6ibr 186	. . . 4 ⊢ (R Fr A → (∀x ∈ A ∀y ∈ A (xRy ∨ x = y ∨ yRx) → R Or A))
61	60	imdistani 340	. . 3 ⊢ ((R Fr A ∧ ∀x ∈ A ∀y ∈ A (xRy ∨ x = y ∨ yRx)) → (R Fr A ∧ R Or A))
62	7, 61	impbi 139	. 2 ⊢ ((R Fr A ∧ R Or A) ↔ (R Fr A ∧ ∀x ∈ A ∀y ∈ A (xRy ∨ x = y ∨ yRx)))
63	1, 62	bitr 151	1 ⊢ (R We A ↔ (R Fr A ∧ ∀x ∈ A ∀y ∈ A (xRy ∨ x = y ∨ yRx)))

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ↔ wb 127 ∨ wo 195 ∧ wa 196 ∨ w3o 580 ∧ w3a 581 ∀wal 672 = weq 797 ∈ wcel 1092 ∀wral 1201 class class class wbr 2054 Po wpo 2058 Or wor 2059 Fr wfr 2061 We wwe 2062

This theorem is referenced by: ordon 2238 weinxp 2467 isowe 2941 f1oweOLD 2944

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-clab 1093 df-cleq 1097 df-clel 1099 df-ral 1205 df-rex 1206 df-v 1349 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-nul 1708 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-br 2063 df-po 2128 df-so 2138 df-fr 2169 df-we 2186

metamath.org