Theorem infmoti 6803

Description: Any class 𝐵 has at most one infimum in 𝐴 (where 𝑅 is interpreted as 'less than'). (Contributed by Jim Kingdon, 18-Dec-2021.)

Hypothesis

Ref	Expression
infmoti.ti	⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))

Assertion

Ref	Expression
infmoti	⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))

Distinct variable groups:   𝑣,𝑢,𝑥,𝑦,𝑧,𝐴   𝑢,𝑅,𝑣,𝑥,𝑦,𝑧   𝑢,𝐵,𝑣,𝑥,𝑦,𝑧   𝜑,𝑢,𝑣,𝑥

Allowed substitution hints:   𝜑(𝑦,𝑧)

Proof of Theorem infmoti

Step	Hyp	Ref	Expression
1		infmoti.ti	. . . 4 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))
2	1	cnvti 6794	. . 3 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢◡𝑅𝑣 ∧ ¬ 𝑣◡𝑅𝑢)))
3	2	supmoti 6768	. 2 ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧)))
4		vex 2636	. . . . . . 7 ⊢ 𝑥 ∈ V
5		vex 2636	. . . . . . 7 ⊢ 𝑦 ∈ V
6	4, 5	brcnv 4650	. . . . . 6 ⊢ (𝑥◡𝑅𝑦 ↔ 𝑦𝑅𝑥)
7	6	notbii 632	. . . . 5 ⊢ (¬ 𝑥◡𝑅𝑦 ↔ ¬ 𝑦𝑅𝑥)
8	7	ralbii 2395	. . . 4 ⊢ (∀𝑦 ∈ 𝐵 ¬ 𝑥◡𝑅𝑦 ↔ ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥)
9	5, 4	brcnv 4650	. . . . . 6 ⊢ (𝑦◡𝑅𝑥 ↔ 𝑥𝑅𝑦)
10		vex 2636	. . . . . . . 8 ⊢ 𝑧 ∈ V
11	5, 10	brcnv 4650	. . . . . . 7 ⊢ (𝑦◡𝑅𝑧 ↔ 𝑧𝑅𝑦)
12	11	rexbii 2396	. . . . . 6 ⊢ (∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧 ↔ ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)
13	9, 12	imbi12i 238	. . . . 5 ⊢ ((𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧) ↔ (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))
14	13	ralbii 2395	. . . 4 ⊢ (∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧) ↔ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))
15	8, 14	anbi12i 449	. . 3 ⊢ ((∀𝑦 ∈ 𝐵 ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧)) ↔ (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))
16	15	rmobii 2571	. 2 ⊢ (∃*𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧)) ↔ ∃*𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))
17	3, 16	sylib 121	1 ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∈ wcel 1445  ∀wral 2370  ∃wrex 2371  ∃*wrmo 2373   class class class wbr 3867  ^◡ccnv 4466

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978  ax-pow 4030  ax-pr 4060

This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-fal 1302  df-nf 1402  df-sb 1700  df-eu 1958  df-mo 1959  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ral 2375  df-rex 2376  df-rmo 2378  df-v 2635  df-un 3017  df-in 3019  df-ss 3026  df-pw 3451  df-sn 3472  df-pr 3473  df-op 3475  df-br 3868  df-opab 3922  df-cnv 4475

This theorem is referenced by:  infeuti  6804