Theorem supclti 7059

Description: A supremum belongs to its base class (closure law). See also supubti 7060 and suplubti 7061. (Contributed by Jim Kingdon, 24-Nov-2021.)

Hypotheses

Ref	Expression
supmoti.ti	⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))
supclti.2	⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))

Assertion

Ref	Expression
supclti	⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ 𝐴)

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

Allowed substitution hints:   𝜑(𝑦,𝑧)   𝐵(𝑣,𝑢)

Proof of Theorem supclti

Step	Hyp	Ref	Expression
1		supmoti.ti	. . 3 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))
2		supclti.2	. . 3 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))
3	1, 2	supval2ti 7056	. 2 ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))))
4	1, 2	supeuti 7055	. . 3 ⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))
5		riotacl 5889	. . 3 ⊢ (∃!𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)) → (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ∈ 𝐴)
6	4, 5	syl 14	. 2 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ∈ 𝐴)
7	3, 6	eqeltrd 2270	1 ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∈ wcel 2164  ∀wral 2472  ∃wrex 2473  ∃!wreu 2474   class class class wbr 4030  ℩crio 5873  supcsup 7043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-reu 2479  df-rmo 2480  df-rab 2481  df-v 2762  df-sbc 2987  df-un 3158  df-in 3160  df-ss 3167  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-iota 5216  df-riota 5874  df-sup 7045

This theorem is referenced by:  suplub2ti  7062  supelti  7063  supisoti  7071  infclti  7084  inflbti  7085  infglbti  7086  suprubex  8972  suprleubex  8975  sup3exmid  8978  suprzclex  9418  supminfex  9665  maxleast  11360  zsupcl  12087  dvdslegcd  12104