Theorem supub 8635

Description: A supremum is an upper bound. See also supcl 8634 and suplub 8636.

This proof demonstrates how to expand an iota-based definition (df-iota 6087) using riotacl2 6880.

(Contributed by NM, 12-Oct-2004.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)

Hypotheses

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

Assertion

Ref	Expression
supub	⊢ (𝜑 → (𝐶 ∈ 𝐵 → ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶))

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

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

Proof of Theorem supub

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 476	. . . . . 6 ⊢ ((∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)) → ∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦)
2	1	a1i 11	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ((∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)) → ∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦))
3	2	ss2rabi 3910	. . . 4 ⊢ {𝑥 ∈ 𝐴 ∣ (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))} ⊆ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦}
4		supmo.1	. . . . . 6 ⊢ (𝜑 → 𝑅 Or 𝐴)
5	4	supval2 8631	. . . . 5 ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))))
6		supcl.2	. . . . . . 7 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))
7	4, 6	supeu 8630	. . . . . 6 ⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))
8		riotacl2 6880	. . . . . 6 ⊢ (∃!𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)) → (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ∈ {𝑥 ∈ 𝐴 ∣ (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))})
9	7, 8	syl 17	. . . . 5 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ∈ {𝑥 ∈ 𝐴 ∣ (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))})
10	5, 9	eqeltrd 2907	. . . 4 ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ {𝑥 ∈ 𝐴 ∣ (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))})
11	3, 10	sseldi 3826	. . 3 ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦})
12		breq2 4878	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (𝑥𝑅𝑦 ↔ 𝑥𝑅𝑤))
13	12	notbid 310	. . . . . . 7 ⊢ (𝑦 = 𝑤 → (¬ 𝑥𝑅𝑦 ↔ ¬ 𝑥𝑅𝑤))
14	13	cbvralv 3384	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ↔ ∀𝑤 ∈ 𝐵 ¬ 𝑥𝑅𝑤)
15		breq1 4877	. . . . . . . 8 ⊢ (𝑥 = sup(𝐵, 𝐴, 𝑅) → (𝑥𝑅𝑤 ↔ sup(𝐵, 𝐴, 𝑅)𝑅𝑤))
16	15	notbid 310	. . . . . . 7 ⊢ (𝑥 = sup(𝐵, 𝐴, 𝑅) → (¬ 𝑥𝑅𝑤 ↔ ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤))
17	16	ralbidv 3196	. . . . . 6 ⊢ (𝑥 = sup(𝐵, 𝐴, 𝑅) → (∀𝑤 ∈ 𝐵 ¬ 𝑥𝑅𝑤 ↔ ∀𝑤 ∈ 𝐵 ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤))
18	14, 17	syl5bb 275	. . . . 5 ⊢ (𝑥 = sup(𝐵, 𝐴, 𝑅) → (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ↔ ∀𝑤 ∈ 𝐵 ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤))
19	18	elrab 3586	. . . 4 ⊢ (sup(𝐵, 𝐴, 𝑅) ∈ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦} ↔ (sup(𝐵, 𝐴, 𝑅) ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐵 ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤))
20	19	simprbi 492	. . 3 ⊢ (sup(𝐵, 𝐴, 𝑅) ∈ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦} → ∀𝑤 ∈ 𝐵 ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤)
21	11, 20	syl 17	. 2 ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤)
22		breq2 4878	. . . 4 ⊢ (𝑤 = 𝐶 → (sup(𝐵, 𝐴, 𝑅)𝑅𝑤 ↔ sup(𝐵, 𝐴, 𝑅)𝑅𝐶))
23	22	notbid 310	. . 3 ⊢ (𝑤 = 𝐶 → (¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤 ↔ ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶))
24	23	rspccv 3524	. 2 ⊢ (∀𝑤 ∈ 𝐵 ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤 → (𝐶 ∈ 𝐵 → ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶))
25	21, 24	syl 17	1 ⊢ (𝜑 → (𝐶 ∈ 𝐵 → ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 386   = wceq 1658   ∈ wcel 2166  ∀wral 3118  ∃wrex 3119  ∃!wreu 3120  {crab 3122   class class class wbr 4874   Or wor 5263  ℩crio 6866  supcsup 8616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ne 3001  df-ral 3123  df-rex 3124  df-reu 3125  df-rmo 3126  df-rab 3127  df-v 3417  df-sbc 3664  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-nul 4146  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4660  df-br 4875  df-po 5264  df-so 5265  df-iota 6087  df-riota 6867  df-sup 8618

This theorem is referenced by:  suplub2  8637  supgtoreq  8646  supiso  8651  inflb  8665  suprub  11315  suprzub  12063  supxrun  12435  supxrub  12443  dgrub  24390  supssd  30036  ssnnssfz  30097  oddpwdc  30962  itg2addnclem  34005  supubt  34078  ssnn0ssfz  42975