Theorem 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	⊢ ( 𝑅 We 𝐴 ↔ ( 𝑅 Fr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-we	⊢ ( 𝑅 We 𝐴 ↔ ( 𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴 ) )
2		df-so	⊢ ( 𝑅 Or 𝐴 ↔ ( 𝑅 Po 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
3		simpr	⊢ ( ( 𝑅 Po 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) )
4		ax-1	⊢ ( 𝑥 𝑅 𝑧 → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
5	4	a1i	⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑥 𝑅 𝑧 → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
6		fr2nr	⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ¬ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) )
7	6	3adantr3	⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ¬ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) )
8		breq2	⊢ ( 𝑥 = 𝑧 → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 𝑧 ) )
9	8	anbi2d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) )
10	9	notbid	⊢ ( 𝑥 = 𝑧 → ( ¬ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ ¬ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) )
11	7 10	syl5ibcom	⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑥 = 𝑧 → ¬ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) )
12		pm2.21	⊢ ( ¬ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
13	11 12	syl6	⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑥 = 𝑧 → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
14		fr3nr	⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ¬ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ∧ 𝑧 𝑅 𝑥 ) )
15		df-3an	⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ∧ 𝑧 𝑅 𝑥 ) ↔ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ∧ 𝑧 𝑅 𝑥 ) )
16	15	biimpri	⊢ ( ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ∧ 𝑧 𝑅 𝑥 ) → ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ∧ 𝑧 𝑅 𝑥 ) )
17	16	ancoms	⊢ ( ( 𝑧 𝑅 𝑥 ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) → ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ∧ 𝑧 𝑅 𝑥 ) )
18	14 17	nsyl	⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ¬ ( 𝑧 𝑅 𝑥 ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) )
19	18	pm2.21d	⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝑧 𝑅 𝑥 ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) → 𝑥 𝑅 𝑧 ) )
20	19	expd	⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑧 𝑅 𝑥 → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
21	5 13 20	3jaod	⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝑥 𝑅 𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧 𝑅 𝑥 ) → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
22		frirr	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 𝑅 𝑥 )
23	22	3ad2antr1	⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ¬ 𝑥 𝑅 𝑥 )
24	21 23	jctild	⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝑥 𝑅 𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧 𝑅 𝑥 ) → ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ) )
25	24	ex	⊢ ( 𝑅 Fr 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑥 𝑅 𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧 𝑅 𝑥 ) → ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ) ) )
26	25	a2d	⊢ ( 𝑅 Fr 𝐴 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧 𝑅 𝑥 ) ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ) ) )
27	26	alimdv	⊢ ( 𝑅 Fr 𝐴 → ( ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧 𝑅 𝑥 ) ) → ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ) ) )
28	27	2alimdv	⊢ ( 𝑅 Fr 𝐴 → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧 𝑅 𝑥 ) ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ) ) )
29		r3al	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑥 𝑅 𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧 𝑅 𝑥 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧 𝑅 𝑥 ) ) )
30		r3al	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ) )
31	28 29 30	3imtr4g	⊢ ( 𝑅 Fr 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑥 𝑅 𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧 𝑅 𝑥 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ) )
32		breq2	⊢ ( 𝑦 = 𝑧 → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑅 𝑧 ) )
33		equequ2	⊢ ( 𝑦 = 𝑧 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑧 ) )
34		breq1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 𝑅 𝑥 ↔ 𝑧 𝑅 𝑥 ) )
35	32 33 34	3orbi123d	⊢ ( 𝑦 = 𝑧 → ( ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ( 𝑥 𝑅 𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧 𝑅 𝑥 ) ) )
36	35	ralidmw	⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) )
37	35	cbvralvw	⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑥 𝑅 𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧 𝑅 𝑥 ) )
38	37	ralbii	⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑥 𝑅 𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧 𝑅 𝑥 ) )
39	36 38	bitr3i	⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑥 𝑅 𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧 𝑅 𝑥 ) )
40	39	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑥 𝑅 𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧 𝑅 𝑥 ) )
41		df-po	⊢ ( 𝑅 Po 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
42	31 40 41	3imtr4g	⊢ ( 𝑅 Fr 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) → 𝑅 Po 𝐴 ) )
43	42	ancrd	⊢ ( 𝑅 Fr 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) → ( 𝑅 Po 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) ) )
44	3 43	impbid2	⊢ ( 𝑅 Fr 𝐴 → ( ( 𝑅 Po 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
45	2 44	bitrid	⊢ ( 𝑅 Fr 𝐴 → ( 𝑅 Or 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
46	45	pm5.32i	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴 ) ↔ ( 𝑅 Fr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
47	1 46	bitri	⊢ ( 𝑅 We 𝐴 ↔ ( 𝑅 Fr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )