Theorem dfwe2 7820

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.)

Assertion

Ref	Expression
dfwe2	⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))

Distinct variable groups:   𝑥,𝑦,𝑅   𝑥,𝐴,𝑦

Proof of Theorem dfwe2

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-we 5613	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
2		df-so 5567	. . . 4 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
3		simpr 490	. . . . 5 ⊢ ((𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))
4		ax1w 13	. . . . . . . . . . . . . 14 ⊢ ((𝑅 Fr 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑧 → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
5		fr2nr 5635	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 Fr 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ¬ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥))
6	5	3adantr3 1190	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 Fr 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ¬ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥))
7		breq2 5112	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑧 → (𝑦𝑅𝑥 ↔ 𝑦𝑅𝑧))
8	7	anbi2d 642	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑧 → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))
9	8	notbid 321	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (¬ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ ¬ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))
10	6, 9	syl5ibcom 248	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 Fr 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥 = 𝑧 → ¬ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))
11		pm2.21 124	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
12	10, 11	syl6 36	. . . . . . . . . . . . . 14 ⊢ ((𝑅 Fr 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥 = 𝑧 → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
13		fr3nr 7818	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 Fr 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ¬ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧 ∧ 𝑧𝑅𝑥))
14		df-3an 1105	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧 ∧ 𝑧𝑅𝑥) ↔ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) ∧ 𝑧𝑅𝑥))
15	14	biimpri 231	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) ∧ 𝑧𝑅𝑥) → (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧 ∧ 𝑧𝑅𝑥))
16	15	ancoms 464	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧𝑅𝑥 ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧 ∧ 𝑧𝑅𝑥))
17	13, 16	nsyl 141	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 Fr 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ¬ (𝑧𝑅𝑥 ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))
18	17	pm2.21d 122	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 Fr 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑧𝑅𝑥 ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧))
19	18	expd 421	. . . . . . . . . . . . . 14 ⊢ ((𝑅 Fr 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑧𝑅𝑥 → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
20	4, 12, 19	3jaod 1457	. . . . . . . . . . . . 13 ⊢ ((𝑅 Fr 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥𝑅𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧𝑅𝑥) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
21		frirr 5634	. . . . . . . . . . . . . 14 ⊢ ((𝑅 Fr 𝐴 ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥𝑅𝑥)
22	21	3ad2antr1 1207	. . . . . . . . . . . . 13 ⊢ ((𝑅 Fr 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ¬ 𝑥𝑅𝑥)
23	20, 22	jctild 535	. . . . . . . . . . . 12 ⊢ ((𝑅 Fr 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥𝑅𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧𝑅𝑥) → (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
24	23	ex 418	. . . . . . . . . . 11 ⊢ (𝑅 Fr 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → ((𝑥𝑅𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧𝑅𝑥) → (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))))
25	24	a2d 30	. . . . . . . . . 10 ⊢ (𝑅 Fr 𝐴 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (𝑥𝑅𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧𝑅𝑥)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))))
26	25	alimdv 1951	. . . . . . . . 9 ⊢ (𝑅 Fr 𝐴 → (∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (𝑥𝑅𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧𝑅𝑥)) → ∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))))
27	26	2alimdv 1953	. . . . . . . 8 ⊢ (𝑅 Fr 𝐴 → (∀𝑥∀𝑦∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (𝑥𝑅𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧𝑅𝑥)) → ∀𝑥∀𝑦∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))))
28		r3al 3204	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧𝑅𝑥) ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (𝑥𝑅𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧𝑅𝑥)))
29		r3al 3204	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
30	27, 28, 29	3imtr4g 299	. . . . . . 7 ⊢ (𝑅 Fr 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧𝑅𝑥) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
31		breq2 5112	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → (𝑥𝑅𝑦 ↔ 𝑥𝑅𝑧))
32		equequ2 2061	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑧))
33		breq1 5111	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → (𝑦𝑅𝑥 ↔ 𝑧𝑅𝑥))
34	31, 32, 33	3orbi123d 1464	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → ((𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ (𝑥𝑅𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧𝑅𝑥)))
35	34	ralidmw 4475	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))
36	34	cbvralvw 3244	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧𝑅𝑥))
37	36	ralbii 3112	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧𝑅𝑥))
38	35, 37	bitr3i 280	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧𝑅𝑥))
39	38	ralbii 3112	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧𝑅𝑥))
40		df-po 5566	. . . . . . 7 ⊢ (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
41	30, 39, 40	3imtr4g 299	. . . . . 6 ⊢ (𝑅 Fr 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) → 𝑅 Po 𝐴))
42	41	ancrd 561	. . . . 5 ⊢ (𝑅 Fr 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) → (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))))
43	3, 42	impbid2 229	. . . 4 ⊢ (𝑅 Fr 𝐴 → ((𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
44	2, 43	bitrid 286	. . 3 ⊢ (𝑅 Fr 𝐴 → (𝑅 Or 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
45	44	pm5.32i 585	. 2 ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴) ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
46	1, 45	bitri 278	1 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ w3o 1102   ∧ w3a 1103  ∀wal 1568   ∈ wcel 2147  ∀wral 3080   class class class wbr 5108   Po wpo 5564   Or wor 5565   Fr wfr 5608   We wwe 5610

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398  ax-un 7783

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4841  df-uni 4873  df-br 5109  df-po 5566  df-so 5567  df-fr 5611  df-we 5613

This theorem is used by:  epweonALT  7822  f1oweALT  8018  fnwe2  8186  dford2  9658  fpwwe2lem11  10765  fpwwe2lem12  10766  vonf1wev  36077  vonf1owevOLD  36079  dfon2  36769