Metamath Proof Explorer

Theorem infmo

Description: Any class B has at most one infimum in A (where R is interpreted as 'less than'). (Contributed by AV, 6-Oct-2020)

Ref Expression
Hypothesis infmo.1 ⊢φ→ROrA
Assertion infmo ⊢φ→∃*x∈A∀y∈B¬yRx∧∀y∈AxRy→∃z∈BzRy

Proof

Step Hyp Ref Expression
1 infmo.1 ⊢φ→ROrA
2 ancom ⊢∀y∈B¬yRx∧∀y∈B¬yRw↔∀y∈B¬yRw∧∀y∈B¬yRx
3 2 anbi2ci ⊢∀y∈B¬yRx∧∀y∈B¬yRw∧∀y∈AwRy→∃z∈BzRy∧∀y∈AxRy→∃z∈BzRy↔∀y∈AwRy→∃z∈BzRy∧∀y∈AxRy→∃z∈BzRy∧∀y∈B¬yRw∧∀y∈B¬yRx
4 an42 ⊢∀y∈B¬yRx∧∀y∈AxRy→∃z∈BzRy∧∀y∈B¬yRw∧∀y∈AwRy→∃z∈BzRy↔∀y∈B¬yRx∧∀y∈B¬yRw∧∀y∈AwRy→∃z∈BzRy∧∀y∈AxRy→∃z∈BzRy
5 an42 ⊢∀y∈AwRy→∃z∈BzRy∧∀y∈B¬yRx∧∀y∈AxRy→∃z∈BzRy∧∀y∈B¬yRw↔∀y∈AwRy→∃z∈BzRy∧∀y∈AxRy→∃z∈BzRy∧∀y∈B¬yRw∧∀y∈B¬yRx
6 3 4 5 3bitr4i ⊢∀y∈B¬yRx∧∀y∈AxRy→∃z∈BzRy∧∀y∈B¬yRw∧∀y∈AwRy→∃z∈BzRy↔∀y∈AwRy→∃z∈BzRy∧∀y∈B¬yRx∧∀y∈AxRy→∃z∈BzRy∧∀y∈B¬yRw
7 ralnex ⊢∀y∈B¬yRx↔¬∃y∈ByRx
8 breq2 ⊢y=x→wRy↔wRx
9 breq2 ⊢y=x→zRy↔zRx
10 9 rexbidv ⊢y=x→∃z∈BzRy↔∃z∈BzRx
11 8 10 imbi12d ⊢y=x→wRy→∃z∈BzRy↔wRx→∃z∈BzRx
12 11 rspcva ⊢x∈A∧∀y∈AwRy→∃z∈BzRy→wRx→∃z∈BzRx
13 breq1 ⊢y=z→yRx↔zRx
14 13 cbvrexvw ⊢∃y∈ByRx↔∃z∈BzRx
15 12 14 syl6ibr ⊢x∈A∧∀y∈AwRy→∃z∈BzRy→wRx→∃y∈ByRx
16 15 con3d ⊢x∈A∧∀y∈AwRy→∃z∈BzRy→¬∃y∈ByRx→¬wRx
17 7 16 biimtrid ⊢x∈A∧∀y∈AwRy→∃z∈BzRy→∀y∈B¬yRx→¬wRx
18 17 expimpd ⊢x∈A→∀y∈AwRy→∃z∈BzRy∧∀y∈B¬yRx→¬wRx
19 18 ad2antrl ⊢ROrA∧x∈A∧w∈A→∀y∈AwRy→∃z∈BzRy∧∀y∈B¬yRx→¬wRx
20 ralnex ⊢∀y∈B¬yRw↔¬∃y∈ByRw
21 breq2 ⊢y=w→xRy↔xRw
22 breq2 ⊢y=w→zRy↔zRw
23 22 rexbidv ⊢y=w→∃z∈BzRy↔∃z∈BzRw
24 21 23 imbi12d ⊢y=w→xRy→∃z∈BzRy↔xRw→∃z∈BzRw
25 24 rspcva ⊢w∈A∧∀y∈AxRy→∃z∈BzRy→xRw→∃z∈BzRw
26 breq1 ⊢y=z→yRw↔zRw
27 26 cbvrexvw ⊢∃y∈ByRw↔∃z∈BzRw
28 25 27 syl6ibr ⊢w∈A∧∀y∈AxRy→∃z∈BzRy→xRw→∃y∈ByRw
29 28 con3d ⊢w∈A∧∀y∈AxRy→∃z∈BzRy→¬∃y∈ByRw→¬xRw
30 20 29 biimtrid ⊢w∈A∧∀y∈AxRy→∃z∈BzRy→∀y∈B¬yRw→¬xRw
31 30 expimpd ⊢w∈A→∀y∈AxRy→∃z∈BzRy∧∀y∈B¬yRw→¬xRw
32 31 ad2antll ⊢ROrA∧x∈A∧w∈A→∀y∈AxRy→∃z∈BzRy∧∀y∈B¬yRw→¬xRw
33 19 32 anim12d ⊢ROrA∧x∈A∧w∈A→∀y∈AwRy→∃z∈BzRy∧∀y∈B¬yRx∧∀y∈AxRy→∃z∈BzRy∧∀y∈B¬yRw→¬wRx∧¬xRw
34 33 imp ⊢ROrA∧x∈A∧w∈A∧∀y∈AwRy→∃z∈BzRy∧∀y∈B¬yRx∧∀y∈AxRy→∃z∈BzRy∧∀y∈B¬yRw→¬wRx∧¬xRw
35 34 ancomd ⊢ROrA∧x∈A∧w∈A∧∀y∈AwRy→∃z∈BzRy∧∀y∈B¬yRx∧∀y∈AxRy→∃z∈BzRy∧∀y∈B¬yRw→¬xRw∧¬wRx
36 35 ex ⊢ROrA∧x∈A∧w∈A→∀y∈AwRy→∃z∈BzRy∧∀y∈B¬yRx∧∀y∈AxRy→∃z∈BzRy∧∀y∈B¬yRw→¬xRw∧¬wRx
37 6 36 biimtrid ⊢ROrA∧x∈A∧w∈A→∀y∈B¬yRx∧∀y∈AxRy→∃z∈BzRy∧∀y∈B¬yRw∧∀y∈AwRy→∃z∈BzRy→¬xRw∧¬wRx
38 sotrieq2 ⊢ROrA∧x∈A∧w∈A→x=w↔¬xRw∧¬wRx
39 37 38 sylibrd ⊢ROrA∧x∈A∧w∈A→∀y∈B¬yRx∧∀y∈AxRy→∃z∈BzRy∧∀y∈B¬yRw∧∀y∈AwRy→∃z∈BzRy→x=w
40 39 ralrimivva ⊢ROrA→∀x∈A∀w∈A∀y∈B¬yRx∧∀y∈AxRy→∃z∈BzRy∧∀y∈B¬yRw∧∀y∈AwRy→∃z∈BzRy→x=w
41 1 40 syl ⊢φ→∀x∈A∀w∈A∀y∈B¬yRx∧∀y∈AxRy→∃z∈BzRy∧∀y∈B¬yRw∧∀y∈AwRy→∃z∈BzRy→x=w
42 breq2 ⊢x=w→yRx↔yRw
43 42 notbid ⊢x=w→¬yRx↔¬yRw
44 43 ralbidv ⊢x=w→∀y∈B¬yRx↔∀y∈B¬yRw
45 breq1 ⊢x=w→xRy↔wRy
46 45 imbi1d ⊢x=w→xRy→∃z∈BzRy↔wRy→∃z∈BzRy
47 46 ralbidv ⊢x=w→∀y∈AxRy→∃z∈BzRy↔∀y∈AwRy→∃z∈BzRy
48 44 47 anbi12d ⊢x=w→∀y∈B¬yRx∧∀y∈AxRy→∃z∈BzRy↔∀y∈B¬yRw∧∀y∈AwRy→∃z∈BzRy
49 48 rmo4 ⊢∃*x∈A∀y∈B¬yRx∧∀y∈AxRy→∃z∈BzRy↔∀x∈A∀w∈A∀y∈B¬yRx∧∀y∈AxRy→∃z∈BzRy∧∀y∈B¬yRw∧∀y∈AwRy→∃z∈BzRy→x=w
50 41 49 sylibr ⊢φ→∃*x∈A∀y∈B¬yRx∧∀y∈AxRy→∃z∈BzRy