Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  supmoti GIF version

Theorem supmoti 6880
 Description: Any class 𝐵 has at most one supremum in 𝐴 (where 𝑅 is interpreted as 'less than'). The hypothesis is satisfied by real numbers (see lttri3 7851) or other orders which correspond to tight apartnesses. (Contributed by Jim Kingdon, 23-Nov-2021.)
Hypothesis
Ref Expression
supmoti.ti ((𝜑 ∧ (𝑢𝐴𝑣𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))
Assertion
Ref Expression
supmoti (𝜑 → ∃*𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)))
Distinct variable groups:   𝑢,𝐴,𝑣,𝑥   𝑦,𝐴,𝑥,𝑧   𝑥,𝐵,𝑦,𝑧   𝑢,𝑅,𝑣,𝑥   𝑦,𝑅,𝑧   𝜑,𝑢,𝑣,𝑥
Allowed substitution hints:   𝜑(𝑦,𝑧)   𝐵(𝑣,𝑢)

Proof of Theorem supmoti
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 ancom 264 . . . . . . 7 ((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦) ↔ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦))
21anbi2ci 454 . . . . . 6 (((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦) ∧ (∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))) ↔ ((∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ∧ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦)))
3 an42 576 . . . . . 6 (((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ∧ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧))) ↔ ((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦) ∧ (∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))))
4 an42 576 . . . . . 6 (((∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦) ∧ (∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦)) ↔ ((∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ∧ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦)))
52, 3, 43bitr4i 211 . . . . 5 (((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ∧ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧))) ↔ ((∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦) ∧ (∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦)))
6 ralnex 2426 . . . . . . . . 9 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ↔ ¬ ∃𝑦𝐵 𝑥𝑅𝑦)
7 breq1 3932 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → (𝑦𝑅𝑤𝑥𝑅𝑤))
8 breq1 3932 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (𝑦𝑅𝑧𝑥𝑅𝑧))
98rexbidv 2438 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → (∃𝑧𝐵 𝑦𝑅𝑧 ↔ ∃𝑧𝐵 𝑥𝑅𝑧))
107, 9imbi12d 233 . . . . . . . . . . . 12 (𝑦 = 𝑥 → ((𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ↔ (𝑥𝑅𝑤 → ∃𝑧𝐵 𝑥𝑅𝑧)))
1110rspcva 2787 . . . . . . . . . . 11 ((𝑥𝐴 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (𝑥𝑅𝑤 → ∃𝑧𝐵 𝑥𝑅𝑧))
12 breq2 3933 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑥𝑅𝑦𝑥𝑅𝑧))
1312cbvrexv 2655 . . . . . . . . . . 11 (∃𝑦𝐵 𝑥𝑅𝑦 ↔ ∃𝑧𝐵 𝑥𝑅𝑧)
1411, 13syl6ibr 161 . . . . . . . . . 10 ((𝑥𝐴 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (𝑥𝑅𝑤 → ∃𝑦𝐵 𝑥𝑅𝑦))
1514con3d 620 . . . . . . . . 9 ((𝑥𝐴 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (¬ ∃𝑦𝐵 𝑥𝑅𝑦 → ¬ 𝑥𝑅𝑤))
166, 15syl5bi 151 . . . . . . . 8 ((𝑥𝐴 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 → ¬ 𝑥𝑅𝑤))
1716expimpd 360 . . . . . . 7 (𝑥𝐴 → ((∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦) → ¬ 𝑥𝑅𝑤))
1817ad2antrl 481 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑤𝐴)) → ((∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦) → ¬ 𝑥𝑅𝑤))
19 ralnex 2426 . . . . . . . . 9 (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ↔ ¬ ∃𝑦𝐵 𝑤𝑅𝑦)
20 breq1 3932 . . . . . . . . . . . . 13 (𝑦 = 𝑤 → (𝑦𝑅𝑥𝑤𝑅𝑥))
21 breq1 3932 . . . . . . . . . . . . . 14 (𝑦 = 𝑤 → (𝑦𝑅𝑧𝑤𝑅𝑧))
2221rexbidv 2438 . . . . . . . . . . . . 13 (𝑦 = 𝑤 → (∃𝑧𝐵 𝑦𝑅𝑧 ↔ ∃𝑧𝐵 𝑤𝑅𝑧))
2320, 22imbi12d 233 . . . . . . . . . . . 12 (𝑦 = 𝑤 → ((𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ↔ (𝑤𝑅𝑥 → ∃𝑧𝐵 𝑤𝑅𝑧)))
2423rspcva 2787 . . . . . . . . . . 11 ((𝑤𝐴 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (𝑤𝑅𝑥 → ∃𝑧𝐵 𝑤𝑅𝑧))
25 breq2 3933 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑤𝑅𝑦𝑤𝑅𝑧))
2625cbvrexv 2655 . . . . . . . . . . 11 (∃𝑦𝐵 𝑤𝑅𝑦 ↔ ∃𝑧𝐵 𝑤𝑅𝑧)
2724, 26syl6ibr 161 . . . . . . . . . 10 ((𝑤𝐴 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (𝑤𝑅𝑥 → ∃𝑦𝐵 𝑤𝑅𝑦))
2827con3d 620 . . . . . . . . 9 ((𝑤𝐴 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (¬ ∃𝑦𝐵 𝑤𝑅𝑦 → ¬ 𝑤𝑅𝑥))
2919, 28syl5bi 151 . . . . . . . 8 ((𝑤𝐴 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 → ¬ 𝑤𝑅𝑥))
3029expimpd 360 . . . . . . 7 (𝑤𝐴 → ((∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦) → ¬ 𝑤𝑅𝑥))
3130ad2antll 482 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑤𝐴)) → ((∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦) → ¬ 𝑤𝑅𝑥))
3218, 31anim12d 333 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑤𝐴)) → (((∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦) ∧ (∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦)) → (¬ 𝑥𝑅𝑤 ∧ ¬ 𝑤𝑅𝑥)))
335, 32syl5bi 151 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑤𝐴)) → (((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ∧ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧))) → (¬ 𝑥𝑅𝑤 ∧ ¬ 𝑤𝑅𝑥)))
34 supmoti.ti . . . . . 6 ((𝜑 ∧ (𝑢𝐴𝑣𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))
3534ralrimivva 2514 . . . . 5 (𝜑 → ∀𝑢𝐴𝑣𝐴 (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))
36 equequ1 1688 . . . . . . 7 (𝑢 = 𝑥 → (𝑢 = 𝑣𝑥 = 𝑣))
37 breq1 3932 . . . . . . . . 9 (𝑢 = 𝑥 → (𝑢𝑅𝑣𝑥𝑅𝑣))
3837notbid 656 . . . . . . . 8 (𝑢 = 𝑥 → (¬ 𝑢𝑅𝑣 ↔ ¬ 𝑥𝑅𝑣))
39 breq2 3933 . . . . . . . . 9 (𝑢 = 𝑥 → (𝑣𝑅𝑢𝑣𝑅𝑥))
4039notbid 656 . . . . . . . 8 (𝑢 = 𝑥 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑣𝑅𝑥))
4138, 40anbi12d 464 . . . . . . 7 (𝑢 = 𝑥 → ((¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢) ↔ (¬ 𝑥𝑅𝑣 ∧ ¬ 𝑣𝑅𝑥)))
4236, 41bibi12d 234 . . . . . 6 (𝑢 = 𝑥 → ((𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)) ↔ (𝑥 = 𝑣 ↔ (¬ 𝑥𝑅𝑣 ∧ ¬ 𝑣𝑅𝑥))))
43 equequ2 1689 . . . . . . 7 (𝑣 = 𝑤 → (𝑥 = 𝑣𝑥 = 𝑤))
44 breq2 3933 . . . . . . . . 9 (𝑣 = 𝑤 → (𝑥𝑅𝑣𝑥𝑅𝑤))
4544notbid 656 . . . . . . . 8 (𝑣 = 𝑤 → (¬ 𝑥𝑅𝑣 ↔ ¬ 𝑥𝑅𝑤))
46 breq1 3932 . . . . . . . . 9 (𝑣 = 𝑤 → (𝑣𝑅𝑥𝑤𝑅𝑥))
4746notbid 656 . . . . . . . 8 (𝑣 = 𝑤 → (¬ 𝑣𝑅𝑥 ↔ ¬ 𝑤𝑅𝑥))
4845, 47anbi12d 464 . . . . . . 7 (𝑣 = 𝑤 → ((¬ 𝑥𝑅𝑣 ∧ ¬ 𝑣𝑅𝑥) ↔ (¬ 𝑥𝑅𝑤 ∧ ¬ 𝑤𝑅𝑥)))
4943, 48bibi12d 234 . . . . . 6 (𝑣 = 𝑤 → ((𝑥 = 𝑣 ↔ (¬ 𝑥𝑅𝑣 ∧ ¬ 𝑣𝑅𝑥)) ↔ (𝑥 = 𝑤 ↔ (¬ 𝑥𝑅𝑤 ∧ ¬ 𝑤𝑅𝑥))))
5042, 49rspc2v 2802 . . . . 5 ((𝑥𝐴𝑤𝐴) → (∀𝑢𝐴𝑣𝐴 (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)) → (𝑥 = 𝑤 ↔ (¬ 𝑥𝑅𝑤 ∧ ¬ 𝑤𝑅𝑥))))
5135, 50mpan9 279 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑤𝐴)) → (𝑥 = 𝑤 ↔ (¬ 𝑥𝑅𝑤 ∧ ¬ 𝑤𝑅𝑥)))
5233, 51sylibrd 168 . . 3 ((𝜑 ∧ (𝑥𝐴𝑤𝐴)) → (((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ∧ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧))) → 𝑥 = 𝑤))
5352ralrimivva 2514 . 2 (𝜑 → ∀𝑥𝐴𝑤𝐴 (((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ∧ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧))) → 𝑥 = 𝑤))
54 breq1 3932 . . . . . 6 (𝑥 = 𝑤 → (𝑥𝑅𝑦𝑤𝑅𝑦))
5554notbid 656 . . . . 5 (𝑥 = 𝑤 → (¬ 𝑥𝑅𝑦 ↔ ¬ 𝑤𝑅𝑦))
5655ralbidv 2437 . . . 4 (𝑥 = 𝑤 → (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ↔ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦))
57 breq2 3933 . . . . . 6 (𝑥 = 𝑤 → (𝑦𝑅𝑥𝑦𝑅𝑤))
5857imbi1d 230 . . . . 5 (𝑥 = 𝑤 → ((𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ↔ (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧)))
5958ralbidv 2437 . . . 4 (𝑥 = 𝑤 → (∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ↔ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧)))
6056, 59anbi12d 464 . . 3 (𝑥 = 𝑤 → ((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ↔ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧))))
6160rmo4 2877 . 2 (∃*𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ↔ ∀𝑥𝐴𝑤𝐴 (((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ∧ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧))) → 𝑥 = 𝑤))
6253, 61sylibr 133 1 (𝜑 → ∃*𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∈ wcel 1480  ∀wral 2416  ∃wrex 2417  ∃*wrmo 2419   class class class wbr 3929 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121 This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-rex 2422  df-rmo 2424  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-br 3930 This theorem is referenced by:  supeuti  6881  infmoti  6915
 Copyright terms: Public domain W3C validator