Theorem supub 9420

Description: A supremum is an upper bound. See also supcl 9419 and suplub 9421.

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

(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 487	. . . . . 6 ⊢ ((∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)) → ∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦)
2	1	a1i 11	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ((∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)) → ∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦))
3	2	ss2rabi 4031	. . . 4 ⊢ {𝑥 ∈ 𝐴 ∣ (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))} ⊆ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦}
4		supmo.1	. . . . . 6 ⊢ (𝜑 → 𝑅 Or 𝐴)
5	4	supval2 9416	. . . . 5 ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))))
6		supcl.2	. . . . . . 7 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))
7	4, 6	supeu 9415	. . . . . 6 ⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))
8		riotacl2 7385	. . . . . 6 ⊢ (∃!𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)) → (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ∈ {𝑥 ∈ 𝐴 ∣ (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))})
9	7, 8	syl 18	. . . . 5 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ∈ {𝑥 ∈ 𝐴 ∣ (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))})
10	5, 9	eqeltrd 2863	. . . 4 ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ {𝑥 ∈ 𝐴 ∣ (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))})
11	3, 10	sselid 3936	. . 3 ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦})
12		breq2 5114	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (𝑥𝑅𝑦 ↔ 𝑥𝑅𝑤))
13	12	notbid 321	. . . . . . 7 ⊢ (𝑦 = 𝑤 → (¬ 𝑥𝑅𝑦 ↔ ¬ 𝑥𝑅𝑤))
14	13	cbvralvw 3243	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ↔ ∀𝑤 ∈ 𝐵 ¬ 𝑥𝑅𝑤)
15		breq1 5113	. . . . . . . 8 ⊢ (𝑥 = sup(𝐵, 𝐴, 𝑅) → (𝑥𝑅𝑤 ↔ sup(𝐵, 𝐴, 𝑅)𝑅𝑤))
16	15	notbid 321	. . . . . . 7 ⊢ (𝑥 = sup(𝐵, 𝐴, 𝑅) → (¬ 𝑥𝑅𝑤 ↔ ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤))
17	16	ralbidv 3188	. . . . . 6 ⊢ (𝑥 = sup(𝐵, 𝐴, 𝑅) → (∀𝑤 ∈ 𝐵 ¬ 𝑥𝑅𝑤 ↔ ∀𝑤 ∈ 𝐵 ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤))
18	14, 17	bitrid 286	. . . . 5 ⊢ (𝑥 = sup(𝐵, 𝐴, 𝑅) → (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ↔ ∀𝑤 ∈ 𝐵 ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤))
19	18	elrab 3651	. . . 4 ⊢ (sup(𝐵, 𝐴, 𝑅) ∈ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦} ↔ (sup(𝐵, 𝐴, 𝑅) ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐵 ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤))
20	19	simprbi 502	. . 3 ⊢ (sup(𝐵, 𝐴, 𝑅) ∈ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦} → ∀𝑤 ∈ 𝐵 ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤)
21	11, 20	syl 18	. 2 ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤)
22		breq2 5114	. . . 4 ⊢ (𝑤 = 𝐶 → (sup(𝐵, 𝐴, 𝑅)𝑅𝑤 ↔ sup(𝐵, 𝐴, 𝑅)𝑅𝐶))
23	22	notbid 321	. . 3 ⊢ (𝑤 = 𝐶 → (¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤 ↔ ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶))
24	23	rspccv 3579	. 2 ⊢ (∀𝑤 ∈ 𝐵 ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤 → (𝐶 ∈ 𝐵 → ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶))
25	21, 24	syl 18	1 ⊢ (𝜑 → (𝐶 ∈ 𝐵 → ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∀wral 3079  ∃wrex 3089  ∃!wreu 3367  {crab 3416   class class class wbr 5110   Or wor 5570  ℩crio 7368  supcsup 9401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-po 5571  df-so 5572  df-iota 6494  df-riota 7369  df-sup 9403

This theorem is referenced by:  suplub2  9422  supssd  9424  supgtoreq  9432  supiso  9437  inflb  9451  suprub  12177  suprzub  12964  supxrun  13343  supxrub  13351  dgrub  26372  ssnnssfz  33110  oddpwdc  34722  itg2addnclem  38300  supubt  38368  supinf  42988  sn-suprubd  43246  ssnn0ssfz  49106