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 syl5bb ( 𝑅 Fr 𝐴 → ( 𝑅 Or 𝐴 ↔ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 𝑅 𝑦𝑥 = 𝑦𝑦 𝑅 𝑥 ) ) )
46 45 pm5.32i ( ( 𝑅 Fr 𝐴𝑅 Or 𝐴 ) ↔ ( 𝑅 Fr 𝐴 ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 𝑅 𝑦𝑥 = 𝑦𝑦 𝑅 𝑥 ) ) )
47 1 46 bitri ( 𝑅 We 𝐴 ↔ ( 𝑅 Fr 𝐴 ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 𝑅 𝑦𝑥 = 𝑦𝑦 𝑅 𝑥 ) ) )