Theorem supnub 9459

Description: An upper bound is not less than the supremum. (Contributed by NM, 13-Oct-2004.)

Hypotheses

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

Assertion

Ref	Expression
supnub	⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐵 ¬ 𝐶𝑅𝑧) → ¬ 𝐶𝑅sup(𝐵, 𝐴, 𝑅)))

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

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

Proof of Theorem supnub

Step	Hyp	Ref	Expression
1		supmo.1	. . . . . 6 ⊢ (𝜑 → 𝑅 Or 𝐴)
2		supcl.2	. . . . . 6 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))
3	1, 2	suplub 9457	. . . . 5 ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ 𝐶𝑅sup(𝐵, 𝐴, 𝑅)) → ∃𝑧 ∈ 𝐵 𝐶𝑅𝑧))
4	3	expdimp 458	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐶𝑅sup(𝐵, 𝐴, 𝑅) → ∃𝑧 ∈ 𝐵 𝐶𝑅𝑧))
5		dfrex2 3089	. . . 4 ⊢ (∃𝑧 ∈ 𝐵 𝐶𝑅𝑧 ↔ ¬ ∀𝑧 ∈ 𝐵 ¬ 𝐶𝑅𝑧)
6	4, 5	imbitrdi 254	. . 3 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐶𝑅sup(𝐵, 𝐴, 𝑅) → ¬ ∀𝑧 ∈ 𝐵 ¬ 𝐶𝑅𝑧))
7	6	con2d 135	. 2 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (∀𝑧 ∈ 𝐵 ¬ 𝐶𝑅𝑧 → ¬ 𝐶𝑅sup(𝐵, 𝐴, 𝑅)))
8	7	expimpd 459	1 ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐵 ¬ 𝐶𝑅𝑧) → ¬ 𝐶𝑅sup(𝐵, 𝐴, 𝑅)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2144  ∀wral 3076  ∃wrex 3086   class class class wbr 5102   Or wor 5557  supcsup 9437

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-po 5558  df-so 5559  df-iota 6496  df-riota 7379  df-sup 9439

This theorem is used by:  supssd  9460  dgrlb  26562  supinf  43400