This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )