Metamath Proof Explorer


Theorem supmo

Description: Any class B has at most one supremum in A (where R is interpreted as 'less than'). (Contributed by NM, 5-May-1999) (Revised by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypothesis supmo.1 ( 𝜑𝑅 Or 𝐴 )
Assertion supmo ( 𝜑 → ∃* 𝑥𝐴 ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 supmo.1 ( 𝜑𝑅 Or 𝐴 )
2 ancom ( ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐵 ¬ 𝑤 𝑅 𝑦 ) ↔ ( ∀ 𝑦𝐵 ¬ 𝑤 𝑅 𝑦 ∧ ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ) )
3 2 anbi2ci ( ( ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐵 ¬ 𝑤 𝑅 𝑦 ) ∧ ( ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) ↔ ( ( ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ∧ ( ∀ 𝑦𝐵 ¬ 𝑤 𝑅 𝑦 ∧ ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ) ) )
4 an42 ( ( ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ∧ ( ∀ 𝑦𝐵 ¬ 𝑤 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) ↔ ( ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐵 ¬ 𝑤 𝑅 𝑦 ) ∧ ( ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) )
5 an42 ( ( ( ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ∧ ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ) ∧ ( ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ∧ ∀ 𝑦𝐵 ¬ 𝑤 𝑅 𝑦 ) ) ↔ ( ( ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ∧ ( ∀ 𝑦𝐵 ¬ 𝑤 𝑅 𝑦 ∧ ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ) ) )
6 3 4 5 3bitr4i ( ( ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ∧ ( ∀ 𝑦𝐵 ¬ 𝑤 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) ↔ ( ( ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ∧ ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ) ∧ ( ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ∧ ∀ 𝑦𝐵 ¬ 𝑤 𝑅 𝑦 ) ) )
7 ralnex ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ↔ ¬ ∃ 𝑦𝐵 𝑥 𝑅 𝑦 )
8 breq1 ( 𝑦 = 𝑥 → ( 𝑦 𝑅 𝑤𝑥 𝑅 𝑤 ) )
9 breq1 ( 𝑦 = 𝑥 → ( 𝑦 𝑅 𝑧𝑥 𝑅 𝑧 ) )
10 9 rexbidv ( 𝑦 = 𝑥 → ( ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ↔ ∃ 𝑧𝐵 𝑥 𝑅 𝑧 ) )
11 8 10 imbi12d ( 𝑦 = 𝑥 → ( ( 𝑦 𝑅 𝑤 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ↔ ( 𝑥 𝑅 𝑤 → ∃ 𝑧𝐵 𝑥 𝑅 𝑧 ) ) )
12 11 rspcva ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) → ( 𝑥 𝑅 𝑤 → ∃ 𝑧𝐵 𝑥 𝑅 𝑧 ) )
13 breq2 ( 𝑦 = 𝑧 → ( 𝑥 𝑅 𝑦𝑥 𝑅 𝑧 ) )
14 13 cbvrexvw ( ∃ 𝑦𝐵 𝑥 𝑅 𝑦 ↔ ∃ 𝑧𝐵 𝑥 𝑅 𝑧 )
15 12 14 syl6ibr ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) → ( 𝑥 𝑅 𝑤 → ∃ 𝑦𝐵 𝑥 𝑅 𝑦 ) )
16 15 con3d ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) → ( ¬ ∃ 𝑦𝐵 𝑥 𝑅 𝑦 → ¬ 𝑥 𝑅 𝑤 ) )
17 7 16 syl5bi ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) → ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 → ¬ 𝑥 𝑅 𝑤 ) )
18 17 expimpd ( 𝑥𝐴 → ( ( ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ∧ ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ) → ¬ 𝑥 𝑅 𝑤 ) )
19 18 ad2antrl ( ( 𝑅 Or 𝐴 ∧ ( 𝑥𝐴𝑤𝐴 ) ) → ( ( ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ∧ ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ) → ¬ 𝑥 𝑅 𝑤 ) )
20 ralnex ( ∀ 𝑦𝐵 ¬ 𝑤 𝑅 𝑦 ↔ ¬ ∃ 𝑦𝐵 𝑤 𝑅 𝑦 )
21 breq1 ( 𝑦 = 𝑤 → ( 𝑦 𝑅 𝑥𝑤 𝑅 𝑥 ) )
22 breq1 ( 𝑦 = 𝑤 → ( 𝑦 𝑅 𝑧𝑤 𝑅 𝑧 ) )
23 22 rexbidv ( 𝑦 = 𝑤 → ( ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ↔ ∃ 𝑧𝐵 𝑤 𝑅 𝑧 ) )
24 21 23 imbi12d ( 𝑦 = 𝑤 → ( ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ↔ ( 𝑤 𝑅 𝑥 → ∃ 𝑧𝐵 𝑤 𝑅 𝑧 ) ) )
25 24 rspcva ( ( 𝑤𝐴 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) → ( 𝑤 𝑅 𝑥 → ∃ 𝑧𝐵 𝑤 𝑅 𝑧 ) )
26 breq2 ( 𝑦 = 𝑧 → ( 𝑤 𝑅 𝑦𝑤 𝑅 𝑧 ) )
27 26 cbvrexvw ( ∃ 𝑦𝐵 𝑤 𝑅 𝑦 ↔ ∃ 𝑧𝐵 𝑤 𝑅 𝑧 )
28 25 27 syl6ibr ( ( 𝑤𝐴 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) → ( 𝑤 𝑅 𝑥 → ∃ 𝑦𝐵 𝑤 𝑅 𝑦 ) )
29 28 con3d ( ( 𝑤𝐴 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) → ( ¬ ∃ 𝑦𝐵 𝑤 𝑅 𝑦 → ¬ 𝑤 𝑅 𝑥 ) )
30 20 29 syl5bi ( ( 𝑤𝐴 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) → ( ∀ 𝑦𝐵 ¬ 𝑤 𝑅 𝑦 → ¬ 𝑤 𝑅 𝑥 ) )
31 30 expimpd ( 𝑤𝐴 → ( ( ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ∧ ∀ 𝑦𝐵 ¬ 𝑤 𝑅 𝑦 ) → ¬ 𝑤 𝑅 𝑥 ) )
32 31 ad2antll ( ( 𝑅 Or 𝐴 ∧ ( 𝑥𝐴𝑤𝐴 ) ) → ( ( ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ∧ ∀ 𝑦𝐵 ¬ 𝑤 𝑅 𝑦 ) → ¬ 𝑤 𝑅 𝑥 ) )
33 19 32 anim12d ( ( 𝑅 Or 𝐴 ∧ ( 𝑥𝐴𝑤𝐴 ) ) → ( ( ( ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ∧ ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ) ∧ ( ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ∧ ∀ 𝑦𝐵 ¬ 𝑤 𝑅 𝑦 ) ) → ( ¬ 𝑥 𝑅 𝑤 ∧ ¬ 𝑤 𝑅 𝑥 ) ) )
34 6 33 syl5bi ( ( 𝑅 Or 𝐴 ∧ ( 𝑥𝐴𝑤𝐴 ) ) → ( ( ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ∧ ( ∀ 𝑦𝐵 ¬ 𝑤 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) → ( ¬ 𝑥 𝑅 𝑤 ∧ ¬ 𝑤 𝑅 𝑥 ) ) )
35 sotrieq2 ( ( 𝑅 Or 𝐴 ∧ ( 𝑥𝐴𝑤𝐴 ) ) → ( 𝑥 = 𝑤 ↔ ( ¬ 𝑥 𝑅 𝑤 ∧ ¬ 𝑤 𝑅 𝑥 ) ) )
36 34 35 sylibrd ( ( 𝑅 Or 𝐴 ∧ ( 𝑥𝐴𝑤𝐴 ) ) → ( ( ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ∧ ( ∀ 𝑦𝐵 ¬ 𝑤 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) → 𝑥 = 𝑤 ) )
37 36 ralrimivva ( 𝑅 Or 𝐴 → ∀ 𝑥𝐴𝑤𝐴 ( ( ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ∧ ( ∀ 𝑦𝐵 ¬ 𝑤 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) → 𝑥 = 𝑤 ) )
38 1 37 syl ( 𝜑 → ∀ 𝑥𝐴𝑤𝐴 ( ( ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ∧ ( ∀ 𝑦𝐵 ¬ 𝑤 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) → 𝑥 = 𝑤 ) )
39 breq1 ( 𝑥 = 𝑤 → ( 𝑥 𝑅 𝑦𝑤 𝑅 𝑦 ) )
40 39 notbid ( 𝑥 = 𝑤 → ( ¬ 𝑥 𝑅 𝑦 ↔ ¬ 𝑤 𝑅 𝑦 ) )
41 40 ralbidv ( 𝑥 = 𝑤 → ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ↔ ∀ 𝑦𝐵 ¬ 𝑤 𝑅 𝑦 ) )
42 breq2 ( 𝑥 = 𝑤 → ( 𝑦 𝑅 𝑥𝑦 𝑅 𝑤 ) )
43 42 imbi1d ( 𝑥 = 𝑤 → ( ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ↔ ( 𝑦 𝑅 𝑤 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) )
44 43 ralbidv ( 𝑥 = 𝑤 → ( ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ↔ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) )
45 41 44 anbi12d ( 𝑥 = 𝑤 → ( ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ↔ ( ∀ 𝑦𝐵 ¬ 𝑤 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) )
46 45 rmo4 ( ∃* 𝑥𝐴 ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ↔ ∀ 𝑥𝐴𝑤𝐴 ( ( ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ∧ ( ∀ 𝑦𝐵 ¬ 𝑤 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) → 𝑥 = 𝑤 ) )
47 38 46 sylibr ( 𝜑 → ∃* 𝑥𝐴 ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) )