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

Theorem supmoti 6399
Description: Any class 𝐵 has at most one supremum in 𝐴 (where 𝑅 is interpreted as 'less than'). The hypothesis is satisfied by real numbers (see lttri3 7157) 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 257 . . . . . . 7 ((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦) ↔ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦))
21anbi2ci 440 . . . . . 6 (((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦) ∧ (∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))) ↔ ((∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ∧ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦)))
3 an42 529 . . . . . 6 (((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ∧ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧))) ↔ ((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦) ∧ (∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))))
4 an42 529 . . . . . 6 (((∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦) ∧ (∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦)) ↔ ((∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ∧ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦)))
52, 3, 43bitr4i 205 . . . . 5 (((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ∧ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧))) ↔ ((∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦) ∧ (∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦)))
6 ralnex 2333 . . . . . . . . 9 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ↔ ¬ ∃𝑦𝐵 𝑥𝑅𝑦)
7 breq1 3795 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → (𝑦𝑅𝑤𝑥𝑅𝑤))
8 breq1 3795 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (𝑦𝑅𝑧𝑥𝑅𝑧))
98rexbidv 2344 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → (∃𝑧𝐵 𝑦𝑅𝑧 ↔ ∃𝑧𝐵 𝑥𝑅𝑧))
107, 9imbi12d 227 . . . . . . . . . . . 12 (𝑦 = 𝑥 → ((𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ↔ (𝑥𝑅𝑤 → ∃𝑧𝐵 𝑥𝑅𝑧)))
1110rspcva 2671 . . . . . . . . . . 11 ((𝑥𝐴 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (𝑥𝑅𝑤 → ∃𝑧𝐵 𝑥𝑅𝑧))
12 breq2 3796 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑥𝑅𝑦𝑥𝑅𝑧))
1312cbvrexv 2551 . . . . . . . . . . 11 (∃𝑦𝐵 𝑥𝑅𝑦 ↔ ∃𝑧𝐵 𝑥𝑅𝑧)
1411, 13syl6ibr 155 . . . . . . . . . 10 ((𝑥𝐴 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (𝑥𝑅𝑤 → ∃𝑦𝐵 𝑥𝑅𝑦))
1514con3d 571 . . . . . . . . 9 ((𝑥𝐴 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (¬ ∃𝑦𝐵 𝑥𝑅𝑦 → ¬ 𝑥𝑅𝑤))
166, 15syl5bi 145 . . . . . . . 8 ((𝑥𝐴 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 → ¬ 𝑥𝑅𝑤))
1716expimpd 349 . . . . . . 7 (𝑥𝐴 → ((∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦) → ¬ 𝑥𝑅𝑤))
1817ad2antrl 467 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑤𝐴)) → ((∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦) → ¬ 𝑥𝑅𝑤))
19 ralnex 2333 . . . . . . . . 9 (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ↔ ¬ ∃𝑦𝐵 𝑤𝑅𝑦)
20 breq1 3795 . . . . . . . . . . . . 13 (𝑦 = 𝑤 → (𝑦𝑅𝑥𝑤𝑅𝑥))
21 breq1 3795 . . . . . . . . . . . . . 14 (𝑦 = 𝑤 → (𝑦𝑅𝑧𝑤𝑅𝑧))
2221rexbidv 2344 . . . . . . . . . . . . 13 (𝑦 = 𝑤 → (∃𝑧𝐵 𝑦𝑅𝑧 ↔ ∃𝑧𝐵 𝑤𝑅𝑧))
2320, 22imbi12d 227 . . . . . . . . . . . 12 (𝑦 = 𝑤 → ((𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ↔ (𝑤𝑅𝑥 → ∃𝑧𝐵 𝑤𝑅𝑧)))
2423rspcva 2671 . . . . . . . . . . 11 ((𝑤𝐴 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (𝑤𝑅𝑥 → ∃𝑧𝐵 𝑤𝑅𝑧))
25 breq2 3796 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑤𝑅𝑦𝑤𝑅𝑧))
2625cbvrexv 2551 . . . . . . . . . . 11 (∃𝑦𝐵 𝑤𝑅𝑦 ↔ ∃𝑧𝐵 𝑤𝑅𝑧)
2724, 26syl6ibr 155 . . . . . . . . . 10 ((𝑤𝐴 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (𝑤𝑅𝑥 → ∃𝑦𝐵 𝑤𝑅𝑦))
2827con3d 571 . . . . . . . . 9 ((𝑤𝐴 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (¬ ∃𝑦𝐵 𝑤𝑅𝑦 → ¬ 𝑤𝑅𝑥))
2919, 28syl5bi 145 . . . . . . . 8 ((𝑤𝐴 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 → ¬ 𝑤𝑅𝑥))
3029expimpd 349 . . . . . . 7 (𝑤𝐴 → ((∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦) → ¬ 𝑤𝑅𝑥))
3130ad2antll 468 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑤𝐴)) → ((∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦) → ¬ 𝑤𝑅𝑥))
3218, 31anim12d 322 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑤𝐴)) → (((∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦) ∧ (∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦)) → (¬ 𝑥𝑅𝑤 ∧ ¬ 𝑤𝑅𝑥)))
335, 32syl5bi 145 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑤𝐴)) → (((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ∧ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧))) → (¬ 𝑥𝑅𝑤 ∧ ¬ 𝑤𝑅𝑥)))
34 supmoti.ti . . . . . 6 ((𝜑 ∧ (𝑢𝐴𝑣𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))
3534ralrimivva 2418 . . . . 5 (𝜑 → ∀𝑢𝐴𝑣𝐴 (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))
36 equequ1 1614 . . . . . . 7 (𝑢 = 𝑥 → (𝑢 = 𝑣𝑥 = 𝑣))
37 breq1 3795 . . . . . . . . 9 (𝑢 = 𝑥 → (𝑢𝑅𝑣𝑥𝑅𝑣))
3837notbid 602 . . . . . . . 8 (𝑢 = 𝑥 → (¬ 𝑢𝑅𝑣 ↔ ¬ 𝑥𝑅𝑣))
39 breq2 3796 . . . . . . . . 9 (𝑢 = 𝑥 → (𝑣𝑅𝑢𝑣𝑅𝑥))
4039notbid 602 . . . . . . . 8 (𝑢 = 𝑥 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑣𝑅𝑥))
4138, 40anbi12d 450 . . . . . . 7 (𝑢 = 𝑥 → ((¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢) ↔ (¬ 𝑥𝑅𝑣 ∧ ¬ 𝑣𝑅𝑥)))
4236, 41bibi12d 228 . . . . . 6 (𝑢 = 𝑥 → ((𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)) ↔ (𝑥 = 𝑣 ↔ (¬ 𝑥𝑅𝑣 ∧ ¬ 𝑣𝑅𝑥))))
43 equequ2 1615 . . . . . . 7 (𝑣 = 𝑤 → (𝑥 = 𝑣𝑥 = 𝑤))
44 breq2 3796 . . . . . . . . 9 (𝑣 = 𝑤 → (𝑥𝑅𝑣𝑥𝑅𝑤))
4544notbid 602 . . . . . . . 8 (𝑣 = 𝑤 → (¬ 𝑥𝑅𝑣 ↔ ¬ 𝑥𝑅𝑤))
46 breq1 3795 . . . . . . . . 9 (𝑣 = 𝑤 → (𝑣𝑅𝑥𝑤𝑅𝑥))
4746notbid 602 . . . . . . . 8 (𝑣 = 𝑤 → (¬ 𝑣𝑅𝑥 ↔ ¬ 𝑤𝑅𝑥))
4845, 47anbi12d 450 . . . . . . 7 (𝑣 = 𝑤 → ((¬ 𝑥𝑅𝑣 ∧ ¬ 𝑣𝑅𝑥) ↔ (¬ 𝑥𝑅𝑤 ∧ ¬ 𝑤𝑅𝑥)))
4943, 48bibi12d 228 . . . . . 6 (𝑣 = 𝑤 → ((𝑥 = 𝑣 ↔ (¬ 𝑥𝑅𝑣 ∧ ¬ 𝑣𝑅𝑥)) ↔ (𝑥 = 𝑤 ↔ (¬ 𝑥𝑅𝑤 ∧ ¬ 𝑤𝑅𝑥))))
5042, 49rspc2v 2685 . . . . 5 ((𝑥𝐴𝑤𝐴) → (∀𝑢𝐴𝑣𝐴 (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)) → (𝑥 = 𝑤 ↔ (¬ 𝑥𝑅𝑤 ∧ ¬ 𝑤𝑅𝑥))))
5135, 50mpan9 269 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑤𝐴)) → (𝑥 = 𝑤 ↔ (¬ 𝑥𝑅𝑤 ∧ ¬ 𝑤𝑅𝑥)))
5233, 51sylibrd 162 . . 3 ((𝜑 ∧ (𝑥𝐴𝑤𝐴)) → (((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ∧ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧))) → 𝑥 = 𝑤))
5352ralrimivva 2418 . 2 (𝜑 → ∀𝑥𝐴𝑤𝐴 (((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ∧ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧))) → 𝑥 = 𝑤))
54 breq1 3795 . . . . . 6 (𝑥 = 𝑤 → (𝑥𝑅𝑦𝑤𝑅𝑦))
5554notbid 602 . . . . 5 (𝑥 = 𝑤 → (¬ 𝑥𝑅𝑦 ↔ ¬ 𝑤𝑅𝑦))
5655ralbidv 2343 . . . 4 (𝑥 = 𝑤 → (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ↔ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦))
57 breq2 3796 . . . . . 6 (𝑥 = 𝑤 → (𝑦𝑅𝑥𝑦𝑅𝑤))
5857imbi1d 224 . . . . 5 (𝑥 = 𝑤 → ((𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ↔ (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧)))
5958ralbidv 2343 . . . 4 (𝑥 = 𝑤 → (∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ↔ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧)))
6056, 59anbi12d 450 . . 3 (𝑥 = 𝑤 → ((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ↔ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧))))
6160rmo4 2757 . 2 (∃*𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ↔ ∀𝑥𝐴𝑤𝐴 (((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ∧ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧))) → 𝑥 = 𝑤))
6253, 61sylibr 141 1 (𝜑 → ∃*𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 101  wb 102  wcel 1409  wral 2323  wrex 2324  ∃*wrmo 2326   class class class wbr 3792
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-fal 1265  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-rex 2329  df-rmo 2331  df-v 2576  df-un 2950  df-sn 3409  df-pr 3410  df-op 3412  df-br 3793
This theorem is referenced by:  supeuti  6400
  Copyright terms: Public domain W3C validator