Theorem supcl 9450

Description: A supremum belongs to its base class (closure law). See also supub 9451 and suplub 9452. (Contributed by NM, 12-Oct-2004.)

Hypotheses

Ref	Expression
supmo.1	⊢ (𝜑 → 𝑅 Or 𝐴)
supcl.2	⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))

Assertion

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

Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝑅,𝑦,𝑧   𝑥,𝐵,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥, 𝑦, 𝑧)

Proof of Theorem supcl

Step	Hyp	Ref	Expression
1		supmo.1	. . 3 ⊢ (𝜑 → 𝑅 Or 𝐴)
2	1	supval2 9447	. 2 ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))))
3		supcl.2	. . . 4 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))
4	1, 3	supeu 9446	. . 3 ⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))
5		riotacl 7394	. . 3 ⊢ (∃!𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)) → (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ∈ 𝐴)
6	4, 5	syl 18	. 2 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ∈ 𝐴)
7	2, 6	eqeltrd 2861	1 ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ 𝐴)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2145  ∀wral 3077  ∃wrex 3087  ∃!wreu 3364   class class class wbr 5103   Or wor 5558  ℩crio 7376  supcsup 9432

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-po 5559  df-so 5560  df-iota 6494  df-riota 7377  df-sup 9434

This theorem is used by:  suplub2  9453  supssd  9455  supiso  9468  infcl  9481  inflb  9482  infglb  9483  infglbb  9484  suprcl  12277  supxrcl  13445  xrsupssd  13463  dgrcl  26552  esum2d  34725  oddpwdc  34986  supclt  38673  supinf  43294  sn-suprcld  43558