Theorem supexpr 10133

Description: The union of a nonempty, bounded set of positive reals has a supremum. Part of Proposition 9-3.3 of [Gleason] p. 122. (Contributed by NM, 19-May-1996.) (New usage is discouraged.)

Assertion

Ref	Expression
supexpr	⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥) → ∃𝑥 ∈ P (∀𝑦 ∈ 𝐴 ¬ 𝑥<P 𝑦 ∧ ∀𝑦 ∈ P (𝑦<P 𝑥 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧)))

Distinct variable group:   𝑥,𝑦,𝑧,𝐴

Proof of Theorem supexpr

Step	Hyp	Ref	Expression
1		suplem1pr 10131	. 2 ⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥) → ∪ 𝐴 ∈ P)
2		ltrelpr 10077	. . . . . . . . 9 ⊢ <P ⊆ (P × P)
3	2	brel 5338	. . . . . . . 8 ⊢ (𝑦<P 𝑥 → (𝑦 ∈ P ∧ 𝑥 ∈ P))
4	3	simpld 488	. . . . . . 7 ⊢ (𝑦<P 𝑥 → 𝑦 ∈ P)
5	4	ralimi 3099	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐴 𝑦<P 𝑥 → ∀𝑦 ∈ 𝐴 𝑦 ∈ P)
6		dfss3 3752	. . . . . 6 ⊢ (𝐴 ⊆ P ↔ ∀𝑦 ∈ 𝐴 𝑦 ∈ P)
7	5, 6	sylibr 225	. . . . 5 ⊢ (∀𝑦 ∈ 𝐴 𝑦<P 𝑥 → 𝐴 ⊆ P)
8	7	rexlimivw 3176	. . . 4 ⊢ (∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥 → 𝐴 ⊆ P)
9	8	adantl 473	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥) → 𝐴 ⊆ P)
10		suplem2pr 10132	. . . . . 6 ⊢ (𝐴 ⊆ P → ((𝑦 ∈ 𝐴 → ¬ ∪ 𝐴<P 𝑦) ∧ (𝑦<P ∪ 𝐴 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧)))
11	10	simpld 488	. . . . 5 ⊢ (𝐴 ⊆ P → (𝑦 ∈ 𝐴 → ¬ ∪ 𝐴<P 𝑦))
12	11	ralrimiv 3112	. . . 4 ⊢ (𝐴 ⊆ P → ∀𝑦 ∈ 𝐴 ¬ ∪ 𝐴<P 𝑦)
13	10	simprd 489	. . . . 5 ⊢ (𝐴 ⊆ P → (𝑦<P ∪ 𝐴 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧))
14	13	ralrimivw 3114	. . . 4 ⊢ (𝐴 ⊆ P → ∀𝑦 ∈ P (𝑦<P ∪ 𝐴 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧))
15	12, 14	jca 507	. . 3 ⊢ (𝐴 ⊆ P → (∀𝑦 ∈ 𝐴 ¬ ∪ 𝐴<P 𝑦 ∧ ∀𝑦 ∈ P (𝑦<P ∪ 𝐴 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧)))
16	9, 15	syl 17	. 2 ⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥) → (∀𝑦 ∈ 𝐴 ¬ ∪ 𝐴<P 𝑦 ∧ ∀𝑦 ∈ P (𝑦<P ∪ 𝐴 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧)))
17		breq1 4814	. . . . . 6 ⊢ (𝑥 = ∪ 𝐴 → (𝑥<P 𝑦 ↔ ∪ 𝐴<P 𝑦))
18	17	notbid 309	. . . . 5 ⊢ (𝑥 = ∪ 𝐴 → (¬ 𝑥<P 𝑦 ↔ ¬ ∪ 𝐴<P 𝑦))
19	18	ralbidv 3133	. . . 4 ⊢ (𝑥 = ∪ 𝐴 → (∀𝑦 ∈ 𝐴 ¬ 𝑥<P 𝑦 ↔ ∀𝑦 ∈ 𝐴 ¬ ∪ 𝐴<P 𝑦))
20		breq2 4815	. . . . . 6 ⊢ (𝑥 = ∪ 𝐴 → (𝑦<P 𝑥 ↔ 𝑦<P ∪ 𝐴))
21	20	imbi1d 332	. . . . 5 ⊢ (𝑥 = ∪ 𝐴 → ((𝑦<P 𝑥 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧) ↔ (𝑦<P ∪ 𝐴 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧)))
22	21	ralbidv 3133	. . . 4 ⊢ (𝑥 = ∪ 𝐴 → (∀𝑦 ∈ P (𝑦<P 𝑥 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧) ↔ ∀𝑦 ∈ P (𝑦<P ∪ 𝐴 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧)))
23	19, 22	anbi12d 624	. . 3 ⊢ (𝑥 = ∪ 𝐴 → ((∀𝑦 ∈ 𝐴 ¬ 𝑥<P 𝑦 ∧ ∀𝑦 ∈ P (𝑦<P 𝑥 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧)) ↔ (∀𝑦 ∈ 𝐴 ¬ ∪ 𝐴<P 𝑦 ∧ ∀𝑦 ∈ P (𝑦<P ∪ 𝐴 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧))))
24	23	rspcev 3462	. 2 ⊢ ((∪ 𝐴 ∈ P ∧ (∀𝑦 ∈ 𝐴 ¬ ∪ 𝐴<P 𝑦 ∧ ∀𝑦 ∈ P (𝑦<P ∪ 𝐴 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧))) → ∃𝑥 ∈ P (∀𝑦 ∈ 𝐴 ¬ 𝑥<P 𝑦 ∧ ∀𝑦 ∈ P (𝑦<P 𝑥 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧)))
25	1, 16, 24	syl2anc 579	1 ⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥) → ∃𝑥 ∈ P (∀𝑦 ∈ 𝐴 ¬ 𝑥<P 𝑦 ∧ ∀𝑦 ∈ P (𝑦<P 𝑥 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 384   = wceq 1652   ∈ wcel 2155   ≠ wne 2937  ∀wral 3055  ∃wrex 3056   ⊆ wss 3734  ∅c0 4081  ∪ cuni 4596   class class class wbr 4811  Pcnp 9938  <_P cltp 9942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151  ax-inf2 8757

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-om 7268  df-1st 7370  df-2nd 7371  df-wrecs 7614  df-recs 7676  df-rdg 7714  df-oadd 7772  df-omul 7773  df-er 7951  df-ni 9951  df-mi 9953  df-lti 9954  df-ltpq 9989  df-enq 9990  df-nq 9991  df-ltnq 9997  df-np 10060  df-ltp 10064

This theorem is referenced by:  supsrlem  10189