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

Theorem supmoti 6609
Description: Any class 𝐵 has at most one supremum in 𝐴 (where 𝑅 is interpreted as 'less than'). The hypothesis is satisfied by real numbers (see lttri3 7486) 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 262 . . . . . . 7 ((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦) ↔ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦))
21anbi2ci 447 . . . . . 6 (((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦) ∧ (∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))) ↔ ((∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ∧ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦)))
3 an42 552 . . . . . 6 (((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ∧ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧))) ↔ ((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦) ∧ (∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))))
4 an42 552 . . . . . 6 (((∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦) ∧ (∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦)) ↔ ((∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ∧ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦)))
52, 3, 43bitr4i 210 . . . . 5 (((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ∧ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧))) ↔ ((∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦) ∧ (∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦)))
6 ralnex 2365 . . . . . . . . 9 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ↔ ¬ ∃𝑦𝐵 𝑥𝑅𝑦)
7 breq1 3817 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → (𝑦𝑅𝑤𝑥𝑅𝑤))
8 breq1 3817 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (𝑦𝑅𝑧𝑥𝑅𝑧))
98rexbidv 2377 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → (∃𝑧𝐵 𝑦𝑅𝑧 ↔ ∃𝑧𝐵 𝑥𝑅𝑧))
107, 9imbi12d 232 . . . . . . . . . . . 12 (𝑦 = 𝑥 → ((𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ↔ (𝑥𝑅𝑤 → ∃𝑧𝐵 𝑥𝑅𝑧)))
1110rspcva 2712 . . . . . . . . . . 11 ((𝑥𝐴 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (𝑥𝑅𝑤 → ∃𝑧𝐵 𝑥𝑅𝑧))
12 breq2 3818 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑥𝑅𝑦𝑥𝑅𝑧))
1312cbvrexv 2586 . . . . . . . . . . 11 (∃𝑦𝐵 𝑥𝑅𝑦 ↔ ∃𝑧𝐵 𝑥𝑅𝑧)
1411, 13syl6ibr 160 . . . . . . . . . 10 ((𝑥𝐴 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (𝑥𝑅𝑤 → ∃𝑦𝐵 𝑥𝑅𝑦))
1514con3d 594 . . . . . . . . 9 ((𝑥𝐴 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (¬ ∃𝑦𝐵 𝑥𝑅𝑦 → ¬ 𝑥𝑅𝑤))
166, 15syl5bi 150 . . . . . . . 8 ((𝑥𝐴 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 → ¬ 𝑥𝑅𝑤))
1716expimpd 355 . . . . . . 7 (𝑥𝐴 → ((∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦) → ¬ 𝑥𝑅𝑤))
1817ad2antrl 474 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑤𝐴)) → ((∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦) → ¬ 𝑥𝑅𝑤))
19 ralnex 2365 . . . . . . . . 9 (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ↔ ¬ ∃𝑦𝐵 𝑤𝑅𝑦)
20 breq1 3817 . . . . . . . . . . . . 13 (𝑦 = 𝑤 → (𝑦𝑅𝑥𝑤𝑅𝑥))
21 breq1 3817 . . . . . . . . . . . . . 14 (𝑦 = 𝑤 → (𝑦𝑅𝑧𝑤𝑅𝑧))
2221rexbidv 2377 . . . . . . . . . . . . 13 (𝑦 = 𝑤 → (∃𝑧𝐵 𝑦𝑅𝑧 ↔ ∃𝑧𝐵 𝑤𝑅𝑧))
2320, 22imbi12d 232 . . . . . . . . . . . 12 (𝑦 = 𝑤 → ((𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ↔ (𝑤𝑅𝑥 → ∃𝑧𝐵 𝑤𝑅𝑧)))
2423rspcva 2712 . . . . . . . . . . 11 ((𝑤𝐴 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (𝑤𝑅𝑥 → ∃𝑧𝐵 𝑤𝑅𝑧))
25 breq2 3818 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑤𝑅𝑦𝑤𝑅𝑧))
2625cbvrexv 2586 . . . . . . . . . . 11 (∃𝑦𝐵 𝑤𝑅𝑦 ↔ ∃𝑧𝐵 𝑤𝑅𝑧)
2724, 26syl6ibr 160 . . . . . . . . . 10 ((𝑤𝐴 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (𝑤𝑅𝑥 → ∃𝑦𝐵 𝑤𝑅𝑦))
2827con3d 594 . . . . . . . . 9 ((𝑤𝐴 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (¬ ∃𝑦𝐵 𝑤𝑅𝑦 → ¬ 𝑤𝑅𝑥))
2919, 28syl5bi 150 . . . . . . . 8 ((𝑤𝐴 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 → ¬ 𝑤𝑅𝑥))
3029expimpd 355 . . . . . . 7 (𝑤𝐴 → ((∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦) → ¬ 𝑤𝑅𝑥))
3130ad2antll 475 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑤𝐴)) → ((∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦) → ¬ 𝑤𝑅𝑥))
3218, 31anim12d 328 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑤𝐴)) → (((∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦) ∧ (∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ∧ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦)) → (¬ 𝑥𝑅𝑤 ∧ ¬ 𝑤𝑅𝑥)))
335, 32syl5bi 150 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑤𝐴)) → (((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ∧ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧))) → (¬ 𝑥𝑅𝑤 ∧ ¬ 𝑤𝑅𝑥)))
34 supmoti.ti . . . . . 6 ((𝜑 ∧ (𝑢𝐴𝑣𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))
3534ralrimivva 2451 . . . . 5 (𝜑 → ∀𝑢𝐴𝑣𝐴 (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))
36 equequ1 1642 . . . . . . 7 (𝑢 = 𝑥 → (𝑢 = 𝑣𝑥 = 𝑣))
37 breq1 3817 . . . . . . . . 9 (𝑢 = 𝑥 → (𝑢𝑅𝑣𝑥𝑅𝑣))
3837notbid 625 . . . . . . . 8 (𝑢 = 𝑥 → (¬ 𝑢𝑅𝑣 ↔ ¬ 𝑥𝑅𝑣))
39 breq2 3818 . . . . . . . . 9 (𝑢 = 𝑥 → (𝑣𝑅𝑢𝑣𝑅𝑥))
4039notbid 625 . . . . . . . 8 (𝑢 = 𝑥 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑣𝑅𝑥))
4138, 40anbi12d 457 . . . . . . 7 (𝑢 = 𝑥 → ((¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢) ↔ (¬ 𝑥𝑅𝑣 ∧ ¬ 𝑣𝑅𝑥)))
4236, 41bibi12d 233 . . . . . 6 (𝑢 = 𝑥 → ((𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)) ↔ (𝑥 = 𝑣 ↔ (¬ 𝑥𝑅𝑣 ∧ ¬ 𝑣𝑅𝑥))))
43 equequ2 1643 . . . . . . 7 (𝑣 = 𝑤 → (𝑥 = 𝑣𝑥 = 𝑤))
44 breq2 3818 . . . . . . . . 9 (𝑣 = 𝑤 → (𝑥𝑅𝑣𝑥𝑅𝑤))
4544notbid 625 . . . . . . . 8 (𝑣 = 𝑤 → (¬ 𝑥𝑅𝑣 ↔ ¬ 𝑥𝑅𝑤))
46 breq1 3817 . . . . . . . . 9 (𝑣 = 𝑤 → (𝑣𝑅𝑥𝑤𝑅𝑥))
4746notbid 625 . . . . . . . 8 (𝑣 = 𝑤 → (¬ 𝑣𝑅𝑥 ↔ ¬ 𝑤𝑅𝑥))
4845, 47anbi12d 457 . . . . . . 7 (𝑣 = 𝑤 → ((¬ 𝑥𝑅𝑣 ∧ ¬ 𝑣𝑅𝑥) ↔ (¬ 𝑥𝑅𝑤 ∧ ¬ 𝑤𝑅𝑥)))
4943, 48bibi12d 233 . . . . . 6 (𝑣 = 𝑤 → ((𝑥 = 𝑣 ↔ (¬ 𝑥𝑅𝑣 ∧ ¬ 𝑣𝑅𝑥)) ↔ (𝑥 = 𝑤 ↔ (¬ 𝑥𝑅𝑤 ∧ ¬ 𝑤𝑅𝑥))))
5042, 49rspc2v 2725 . . . . 5 ((𝑥𝐴𝑤𝐴) → (∀𝑢𝐴𝑣𝐴 (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)) → (𝑥 = 𝑤 ↔ (¬ 𝑥𝑅𝑤 ∧ ¬ 𝑤𝑅𝑥))))
5135, 50mpan9 275 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑤𝐴)) → (𝑥 = 𝑤 ↔ (¬ 𝑥𝑅𝑤 ∧ ¬ 𝑤𝑅𝑥)))
5233, 51sylibrd 167 . . 3 ((𝜑 ∧ (𝑥𝐴𝑤𝐴)) → (((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ∧ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧))) → 𝑥 = 𝑤))
5352ralrimivva 2451 . 2 (𝜑 → ∀𝑥𝐴𝑤𝐴 (((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ∧ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧))) → 𝑥 = 𝑤))
54 breq1 3817 . . . . . 6 (𝑥 = 𝑤 → (𝑥𝑅𝑦𝑤𝑅𝑦))
5554notbid 625 . . . . 5 (𝑥 = 𝑤 → (¬ 𝑥𝑅𝑦 ↔ ¬ 𝑤𝑅𝑦))
5655ralbidv 2376 . . . 4 (𝑥 = 𝑤 → (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ↔ ∀𝑦𝐵 ¬ 𝑤𝑅𝑦))
57 breq2 3818 . . . . . 6 (𝑥 = 𝑤 → (𝑦𝑅𝑥𝑦𝑅𝑤))
5857imbi1d 229 . . . . 5 (𝑥 = 𝑤 → ((𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ↔ (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧)))
5958ralbidv 2376 . . . 4 (𝑥 = 𝑤 → (∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ↔ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧)))
6056, 59anbi12d 457 . . 3 (𝑥 = 𝑤 → ((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ↔ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧))))
6160rmo4 2798 . 2 (∃*𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ↔ ∀𝑥𝐴𝑤𝐴 (((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ∧ (∀𝑦𝐵 ¬ 𝑤𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑤 → ∃𝑧𝐵 𝑦𝑅𝑧))) → 𝑥 = 𝑤))
6253, 61sylibr 132 1 (𝜑 → ∃*𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wb 103  wcel 1436  wral 2355  wrex 2356  ∃*wrmo 2358   class class class wbr 3814
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-rex 2361  df-rmo 2363  df-v 2616  df-un 2990  df-sn 3431  df-pr 3432  df-op 3434  df-br 3815
This theorem is referenced by:  supeuti  6610  infmoti  6644
  Copyright terms: Public domain W3C validator