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 imbitrrdi ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ( 𝑥 𝑅 𝑤 → ∃ 𝑦 ∈ 𝐵 𝑥 𝑅 𝑦 ) )
16 15 con3d ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ( ¬ ∃ 𝑦 ∈ 𝐵 𝑥 𝑅 𝑦 → ¬ 𝑥 𝑅 𝑤 ) )
17 7 16 biimtrid ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 → ¬ 𝑥 𝑅 𝑤 ) )
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 imbitrrdi ⊢ ( ( 𝑤 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ( 𝑤 𝑅 𝑥 → ∃ 𝑦 ∈ 𝐵 𝑤 𝑅 𝑦 ) )
29 28 con3d ⊢ ( ( 𝑤 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ( ¬ ∃ 𝑦 ∈ 𝐵 𝑤 𝑅 𝑦 → ¬ 𝑤 𝑅 𝑥 ) )
30 20 29 biimtrid ⊢ ( ( 𝑤 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑤 𝑅 𝑦 → ¬ 𝑤 𝑅 𝑥 ) )
31 30 expimpd ⊢ ( 𝑤 ∈ 𝐴 → ( ( ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑤 𝑅 𝑦 ) → ¬ 𝑤 𝑅 𝑥 ) )
32 31 ad2antll ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑤 𝑅 𝑦 ) → ¬ 𝑤 𝑅 𝑥 ) )
33 19 32 anim12d ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( ( ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑤 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑤 𝑅 𝑦 ) ) → ( ¬ 𝑥 𝑅 𝑤 ∧ ¬ 𝑤 𝑅 𝑥 ) ) )
34 6 33 biimtrid ⊢ ( ( 𝑅 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 ⊢ ( 𝜑 → ∃* 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )