MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  drsdirfi Structured version   Visualization version   GIF version
Theorem drsdirfi 18258
Description: Any finite number of elements in a directed set have a common upper bound. Here is where the nonemptiness constraint in df-drs 18249 first comes into play; without it we would need an additional constraint that 𝑋 not be empty. (Contributed by Stefan O'Rear, 1-Feb-2015.)
Hypotheses
Ref Expression
drsbn0.b 𝐡 = (Baseβ€˜πΎ)
drsdirfi.l ≀ = (leβ€˜πΎ)
Assertion
Ref Expression
drsdirfi ((𝐾 ∈ Dirset ∧ 𝑋 βŠ† 𝐡 ∧ 𝑋 ∈ Fin) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑋 𝑧 ≀ 𝑦)
Distinct variable groups:   𝑦,𝐾,𝑧   𝑦,𝐡,𝑧   𝑦, ≀ ,𝑧   𝑦,𝑋,𝑧
Proof of Theorem drsdirfi
Dummy variables π‘Ž 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sseq1 4008 . . . . . 6 (π‘Ž = βˆ… β†’ (π‘Ž βŠ† 𝐡 ↔ βˆ… βŠ† 𝐡))
21anbi2d 630 . . . . 5 (π‘Ž = βˆ… β†’ ((𝐾 ∈ Dirset ∧ π‘Ž βŠ† 𝐡) ↔ (𝐾 ∈ Dirset ∧ βˆ… βŠ† 𝐡)))
3 raleq 3323 . . . . . 6 (π‘Ž = βˆ… β†’ (βˆ€π‘§ ∈ π‘Ž 𝑧 ≀ 𝑦 ↔ βˆ€π‘§ ∈ βˆ… 𝑧 ≀ 𝑦))
43rexbidv 3179 . . . . 5 (π‘Ž = βˆ… β†’ (βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ π‘Ž 𝑧 ≀ 𝑦 ↔ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ βˆ… 𝑧 ≀ 𝑦))
52, 4imbi12d 345 . . . 4 (π‘Ž = βˆ… β†’ (((𝐾 ∈ Dirset ∧ π‘Ž βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ π‘Ž 𝑧 ≀ 𝑦) ↔ ((𝐾 ∈ Dirset ∧ βˆ… βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ βˆ… 𝑧 ≀ 𝑦)))
6 sseq1 4008 . . . . . 6 (π‘Ž = 𝑏 β†’ (π‘Ž βŠ† 𝐡 ↔ 𝑏 βŠ† 𝐡))
76anbi2d 630 . . . . 5 (π‘Ž = 𝑏 β†’ ((𝐾 ∈ Dirset ∧ π‘Ž βŠ† 𝐡) ↔ (𝐾 ∈ Dirset ∧ 𝑏 βŠ† 𝐡)))
8 raleq 3323 . . . . . 6 (π‘Ž = 𝑏 β†’ (βˆ€π‘§ ∈ π‘Ž 𝑧 ≀ 𝑦 ↔ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ 𝑦))
98rexbidv 3179 . . . . 5 (π‘Ž = 𝑏 β†’ (βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ π‘Ž 𝑧 ≀ 𝑦 ↔ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑏 𝑧 ≀ 𝑦))
107, 9imbi12d 345 . . . 4 (π‘Ž = 𝑏 β†’ (((𝐾 ∈ Dirset ∧ π‘Ž βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ π‘Ž 𝑧 ≀ 𝑦) ↔ ((𝐾 ∈ Dirset ∧ 𝑏 βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑏 𝑧 ≀ 𝑦)))
11 sseq1 4008 . . . . . 6 (π‘Ž = (𝑏 βˆͺ {𝑐}) β†’ (π‘Ž βŠ† 𝐡 ↔ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡))
1211anbi2d 630 . . . . 5 (π‘Ž = (𝑏 βˆͺ {𝑐}) β†’ ((𝐾 ∈ Dirset ∧ π‘Ž βŠ† 𝐡) ↔ (𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡)))
13 raleq 3323 . . . . . 6 (π‘Ž = (𝑏 βˆͺ {𝑐}) β†’ (βˆ€π‘§ ∈ π‘Ž 𝑧 ≀ 𝑦 ↔ βˆ€π‘§ ∈ (𝑏 βˆͺ {𝑐})𝑧 ≀ 𝑦))
1413rexbidv 3179 . . . . 5 (π‘Ž = (𝑏 βˆͺ {𝑐}) β†’ (βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ π‘Ž 𝑧 ≀ 𝑦 ↔ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ (𝑏 βˆͺ {𝑐})𝑧 ≀ 𝑦))
1512, 14imbi12d 345 . . . 4 (π‘Ž = (𝑏 βˆͺ {𝑐}) β†’ (((𝐾 ∈ Dirset ∧ π‘Ž βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ π‘Ž 𝑧 ≀ 𝑦) ↔ ((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ (𝑏 βˆͺ {𝑐})𝑧 ≀ 𝑦)))
16 sseq1 4008 . . . . . 6 (π‘Ž = 𝑋 β†’ (π‘Ž βŠ† 𝐡 ↔ 𝑋 βŠ† 𝐡))
1716anbi2d 630 . . . . 5 (π‘Ž = 𝑋 β†’ ((𝐾 ∈ Dirset ∧ π‘Ž βŠ† 𝐡) ↔ (𝐾 ∈ Dirset ∧ 𝑋 βŠ† 𝐡)))
18 raleq 3323 . . . . . 6 (π‘Ž = 𝑋 β†’ (βˆ€π‘§ ∈ π‘Ž 𝑧 ≀ 𝑦 ↔ βˆ€π‘§ ∈ 𝑋 𝑧 ≀ 𝑦))
1918rexbidv 3179 . . . . 5 (π‘Ž = 𝑋 β†’ (βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ π‘Ž 𝑧 ≀ 𝑦 ↔ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑋 𝑧 ≀ 𝑦))
2017, 19imbi12d 345 . . . 4 (π‘Ž = 𝑋 β†’ (((𝐾 ∈ Dirset ∧ π‘Ž βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ π‘Ž 𝑧 ≀ 𝑦) ↔ ((𝐾 ∈ Dirset ∧ 𝑋 βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑋 𝑧 ≀ 𝑦)))
21 drsbn0.b . . . . . . 7 𝐡 = (Baseβ€˜πΎ)
2221drsbn0 18257 . . . . . 6 (𝐾 ∈ Dirset β†’ 𝐡 β‰  βˆ…)
23 ral0 4513 . . . . . . . . 9 βˆ€π‘§ ∈ βˆ… 𝑧 ≀ 𝑦
2423jctr 526 . . . . . . . 8 (𝑦 ∈ 𝐡 β†’ (𝑦 ∈ 𝐡 ∧ βˆ€π‘§ ∈ βˆ… 𝑧 ≀ 𝑦))
2524eximi 1838 . . . . . . 7 (βˆƒπ‘¦ 𝑦 ∈ 𝐡 β†’ βˆƒπ‘¦(𝑦 ∈ 𝐡 ∧ βˆ€π‘§ ∈ βˆ… 𝑧 ≀ 𝑦))
26 n0 4347 . . . . . . 7 (𝐡 β‰  βˆ… ↔ βˆƒπ‘¦ 𝑦 ∈ 𝐡)
27 df-rex 3072 . . . . . . 7 (βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ βˆ… 𝑧 ≀ 𝑦 ↔ βˆƒπ‘¦(𝑦 ∈ 𝐡 ∧ βˆ€π‘§ ∈ βˆ… 𝑧 ≀ 𝑦))
2825, 26, 273imtr4i 292 . . . . . 6 (𝐡 β‰  βˆ… β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ βˆ… 𝑧 ≀ 𝑦)
2922, 28syl 17 . . . . 5 (𝐾 ∈ Dirset β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ βˆ… 𝑧 ≀ 𝑦)
3029adantr 482 . . . 4 ((𝐾 ∈ Dirset ∧ βˆ… βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ βˆ… 𝑧 ≀ 𝑦)
31 ssun1 4173 . . . . . . . . 9 𝑏 βŠ† (𝑏 βˆͺ {𝑐})
32 sstr 3991 . . . . . . . . 9 ((𝑏 βŠ† (𝑏 βˆͺ {𝑐}) ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) β†’ 𝑏 βŠ† 𝐡)
3331, 32mpan 689 . . . . . . . 8 ((𝑏 βˆͺ {𝑐}) βŠ† 𝐡 β†’ 𝑏 βŠ† 𝐡)
3433anim2i 618 . . . . . . 7 ((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) β†’ (𝐾 ∈ Dirset ∧ 𝑏 βŠ† 𝐡))
35 breq2 5153 . . . . . . . . . 10 (𝑦 = π‘Ž β†’ (𝑧 ≀ 𝑦 ↔ 𝑧 ≀ π‘Ž))
3635ralbidv 3178 . . . . . . . . 9 (𝑦 = π‘Ž β†’ (βˆ€π‘§ ∈ 𝑏 𝑧 ≀ 𝑦 ↔ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž))
3736cbvrexvw 3236 . . . . . . . 8 (βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑏 𝑧 ≀ 𝑦 ↔ βˆƒπ‘Ž ∈ 𝐡 βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)
38 simplrr 777 . . . . . . . . . . . 12 ((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ (π‘Ž ∈ 𝐡 ∧ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) β†’ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)
39 drsprs 18256 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ Dirset β†’ 𝐾 ∈ Proset )
4039ad5antr 733 . . . . . . . . . . . . . . . 16 ((((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) ∧ 𝑧 ∈ 𝑏) ∧ 𝑧 ≀ π‘Ž) β†’ 𝐾 ∈ Proset )
4133ad2antlr 726 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) β†’ 𝑏 βŠ† 𝐡)
4241adantr 482 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) β†’ 𝑏 βŠ† 𝐡)
4342sselda 3983 . . . . . . . . . . . . . . . . 17 (((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) ∧ 𝑧 ∈ 𝑏) β†’ 𝑧 ∈ 𝐡)
4443adantr 482 . . . . . . . . . . . . . . . 16 ((((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) ∧ 𝑧 ∈ 𝑏) ∧ 𝑧 ≀ π‘Ž) β†’ 𝑧 ∈ 𝐡)
45 simp-4r 783 . . . . . . . . . . . . . . . 16 ((((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) ∧ 𝑧 ∈ 𝑏) ∧ 𝑧 ≀ π‘Ž) β†’ π‘Ž ∈ 𝐡)
46 simprl 770 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) β†’ 𝑦 ∈ 𝐡)
4746ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) ∧ 𝑧 ∈ 𝑏) ∧ 𝑧 ≀ π‘Ž) β†’ 𝑦 ∈ 𝐡)
48 simpr 486 . . . . . . . . . . . . . . . 16 ((((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) ∧ 𝑧 ∈ 𝑏) ∧ 𝑧 ≀ π‘Ž) β†’ 𝑧 ≀ π‘Ž)
49 simprrl 780 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) β†’ π‘Ž ≀ 𝑦)
5049ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) ∧ 𝑧 ∈ 𝑏) ∧ 𝑧 ≀ π‘Ž) β†’ π‘Ž ≀ 𝑦)
51 drsdirfi.l . . . . . . . . . . . . . . . . 17 ≀ = (leβ€˜πΎ)
5221, 51prstr 18253 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Proset ∧ (𝑧 ∈ 𝐡 ∧ π‘Ž ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ (𝑧 ≀ π‘Ž ∧ π‘Ž ≀ 𝑦)) β†’ 𝑧 ≀ 𝑦)
5340, 44, 45, 47, 48, 50, 52syl132anc 1389 . . . . . . . . . . . . . . 15 ((((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) ∧ 𝑧 ∈ 𝑏) ∧ 𝑧 ≀ π‘Ž) β†’ 𝑧 ≀ 𝑦)
5453ex 414 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) ∧ 𝑧 ∈ 𝑏) β†’ (𝑧 ≀ π‘Ž β†’ 𝑧 ≀ 𝑦))
5554ralimdva 3168 . . . . . . . . . . . . 13 ((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) β†’ (βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž β†’ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ 𝑦))
5655adantlrr 720 . . . . . . . . . . . 12 ((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ (π‘Ž ∈ 𝐡 ∧ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) β†’ (βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž β†’ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ 𝑦))
5738, 56mpd 15 . . . . . . . . . . 11 ((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ (π‘Ž ∈ 𝐡 ∧ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) β†’ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ 𝑦)
58 simprrr 781 . . . . . . . . . . . 12 ((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ (π‘Ž ∈ 𝐡 ∧ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) β†’ 𝑐 ≀ 𝑦)
59 vex 3479 . . . . . . . . . . . . 13 𝑐 ∈ V
60 breq1 5152 . . . . . . . . . . . . 13 (𝑧 = 𝑐 β†’ (𝑧 ≀ 𝑦 ↔ 𝑐 ≀ 𝑦))
6159, 60ralsn 4686 . . . . . . . . . . . 12 (βˆ€π‘§ ∈ {𝑐}𝑧 ≀ 𝑦 ↔ 𝑐 ≀ 𝑦)
6258, 61sylibr 233 . . . . . . . . . . 11 ((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ (π‘Ž ∈ 𝐡 ∧ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) β†’ βˆ€π‘§ ∈ {𝑐}𝑧 ≀ 𝑦)
63 ralun 4193 . . . . . . . . . . 11 ((βˆ€π‘§ ∈ 𝑏 𝑧 ≀ 𝑦 ∧ βˆ€π‘§ ∈ {𝑐}𝑧 ≀ 𝑦) β†’ βˆ€π‘§ ∈ (𝑏 βˆͺ {𝑐})𝑧 ≀ 𝑦)
6457, 62, 63syl2anc 585 . . . . . . . . . 10 ((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ (π‘Ž ∈ 𝐡 ∧ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) β†’ βˆ€π‘§ ∈ (𝑏 βˆͺ {𝑐})𝑧 ≀ 𝑦)
65 simpll 766 . . . . . . . . . . 11 (((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ (π‘Ž ∈ 𝐡 ∧ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)) β†’ 𝐾 ∈ Dirset)
66 simprl 770 . . . . . . . . . . 11 (((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ (π‘Ž ∈ 𝐡 ∧ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)) β†’ π‘Ž ∈ 𝐡)
67 ssun2 4174 . . . . . . . . . . . . . 14 {𝑐} βŠ† (𝑏 βˆͺ {𝑐})
68 sstr 3991 . . . . . . . . . . . . . 14 (({𝑐} βŠ† (𝑏 βˆͺ {𝑐}) ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) β†’ {𝑐} βŠ† 𝐡)
6967, 68mpan 689 . . . . . . . . . . . . 13 ((𝑏 βˆͺ {𝑐}) βŠ† 𝐡 β†’ {𝑐} βŠ† 𝐡)
7059snss 4790 . . . . . . . . . . . . 13 (𝑐 ∈ 𝐡 ↔ {𝑐} βŠ† 𝐡)
7169, 70sylibr 233 . . . . . . . . . . . 12 ((𝑏 βˆͺ {𝑐}) βŠ† 𝐡 β†’ 𝑐 ∈ 𝐡)
7271ad2antlr 726 . . . . . . . . . . 11 (((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ (π‘Ž ∈ 𝐡 ∧ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)) β†’ 𝑐 ∈ 𝐡)
7321, 51drsdir 18255 . . . . . . . . . . 11 ((𝐾 ∈ Dirset ∧ π‘Ž ∈ 𝐡 ∧ 𝑐 ∈ 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))
7465, 66, 72, 73syl3anc 1372 . . . . . . . . . 10 (((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ (π‘Ž ∈ 𝐡 ∧ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)) β†’ βˆƒπ‘¦ ∈ 𝐡 (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))
7564, 74reximddv 3172 . . . . . . . . 9 (((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ (π‘Ž ∈ 𝐡 ∧ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ (𝑏 βˆͺ {𝑐})𝑧 ≀ 𝑦)
7675rexlimdvaa 3157 . . . . . . . 8 ((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) β†’ (βˆƒπ‘Ž ∈ 𝐡 βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ (𝑏 βˆͺ {𝑐})𝑧 ≀ 𝑦))
7737, 76biimtrid 241 . . . . . . 7 ((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) β†’ (βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑏 𝑧 ≀ 𝑦 β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ (𝑏 βˆͺ {𝑐})𝑧 ≀ 𝑦))
7834, 77embantd 59 . . . . . 6 ((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) β†’ (((𝐾 ∈ Dirset ∧ 𝑏 βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑏 𝑧 ≀ 𝑦) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ (𝑏 βˆͺ {𝑐})𝑧 ≀ 𝑦))
7978com12 32 . . . . 5 (((𝐾 ∈ Dirset ∧ 𝑏 βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑏 𝑧 ≀ 𝑦) β†’ ((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ (𝑏 βˆͺ {𝑐})𝑧 ≀ 𝑦))
8079a1i 11 . . . 4 (𝑏 ∈ Fin β†’ (((𝐾 ∈ Dirset ∧ 𝑏 βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑏 𝑧 ≀ 𝑦) β†’ ((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ (𝑏 βˆͺ {𝑐})𝑧 ≀ 𝑦)))
815, 10, 15, 20, 30, 80findcard2 9164 . . 3 (𝑋 ∈ Fin β†’ ((𝐾 ∈ Dirset ∧ 𝑋 βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑋 𝑧 ≀ 𝑦))
8281com12 32 . 2 ((𝐾 ∈ Dirset ∧ 𝑋 βŠ† 𝐡) β†’ (𝑋 ∈ Fin β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑋 𝑧 ≀ 𝑦))
83823impia 1118 1 ((𝐾 ∈ Dirset ∧ 𝑋 βŠ† 𝐡 ∧ 𝑋 ∈ Fin) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑋 𝑧 ≀ 𝑦)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071   βˆͺ cun 3947   βŠ† wss 3949  βˆ…c0 4323  {csn 4629   class class class wbr 5149  β€˜cfv 6544  Fincfn 8939  Basecbs 17144  lecple 17204   Proset cproset 18246  Dirsetcdrs 18247
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-om 7856  df-en 8940  df-fin 8943  df-proset 18248  df-drs 18249
This theorem is referenced by:  isdrs2  18259  ipodrsfi  18492
  Copyright terms: Public domain W3C validator