MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  drsdirfi Structured version   Visualization version   GIF version

Theorem drsdirfi 18262
Description: Any finite number of elements in a directed set have a common upper bound. Here is where the nonemptiness constraint in df-drs 18253 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 4006 . . . . . 6 (π‘Ž = βˆ… β†’ (π‘Ž βŠ† 𝐡 ↔ βˆ… βŠ† 𝐡))
21anbi2d 627 . . . . 5 (π‘Ž = βˆ… β†’ ((𝐾 ∈ Dirset ∧ π‘Ž βŠ† 𝐡) ↔ (𝐾 ∈ Dirset ∧ βˆ… βŠ† 𝐡)))
3 raleq 3320 . . . . . 6 (π‘Ž = βˆ… β†’ (βˆ€π‘§ ∈ π‘Ž 𝑧 ≀ 𝑦 ↔ βˆ€π‘§ ∈ βˆ… 𝑧 ≀ 𝑦))
43rexbidv 3176 . . . . 5 (π‘Ž = βˆ… β†’ (βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ π‘Ž 𝑧 ≀ 𝑦 ↔ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ βˆ… 𝑧 ≀ 𝑦))
52, 4imbi12d 343 . . . 4 (π‘Ž = βˆ… β†’ (((𝐾 ∈ Dirset ∧ π‘Ž βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ π‘Ž 𝑧 ≀ 𝑦) ↔ ((𝐾 ∈ Dirset ∧ βˆ… βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ βˆ… 𝑧 ≀ 𝑦)))
6 sseq1 4006 . . . . . 6 (π‘Ž = 𝑏 β†’ (π‘Ž βŠ† 𝐡 ↔ 𝑏 βŠ† 𝐡))
76anbi2d 627 . . . . 5 (π‘Ž = 𝑏 β†’ ((𝐾 ∈ Dirset ∧ π‘Ž βŠ† 𝐡) ↔ (𝐾 ∈ Dirset ∧ 𝑏 βŠ† 𝐡)))
8 raleq 3320 . . . . . 6 (π‘Ž = 𝑏 β†’ (βˆ€π‘§ ∈ π‘Ž 𝑧 ≀ 𝑦 ↔ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ 𝑦))
98rexbidv 3176 . . . . 5 (π‘Ž = 𝑏 β†’ (βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ π‘Ž 𝑧 ≀ 𝑦 ↔ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑏 𝑧 ≀ 𝑦))
107, 9imbi12d 343 . . . 4 (π‘Ž = 𝑏 β†’ (((𝐾 ∈ Dirset ∧ π‘Ž βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ π‘Ž 𝑧 ≀ 𝑦) ↔ ((𝐾 ∈ Dirset ∧ 𝑏 βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑏 𝑧 ≀ 𝑦)))
11 sseq1 4006 . . . . . 6 (π‘Ž = (𝑏 βˆͺ {𝑐}) β†’ (π‘Ž βŠ† 𝐡 ↔ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡))
1211anbi2d 627 . . . . 5 (π‘Ž = (𝑏 βˆͺ {𝑐}) β†’ ((𝐾 ∈ Dirset ∧ π‘Ž βŠ† 𝐡) ↔ (𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡)))
13 raleq 3320 . . . . . 6 (π‘Ž = (𝑏 βˆͺ {𝑐}) β†’ (βˆ€π‘§ ∈ π‘Ž 𝑧 ≀ 𝑦 ↔ βˆ€π‘§ ∈ (𝑏 βˆͺ {𝑐})𝑧 ≀ 𝑦))
1413rexbidv 3176 . . . . 5 (π‘Ž = (𝑏 βˆͺ {𝑐}) β†’ (βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ π‘Ž 𝑧 ≀ 𝑦 ↔ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ (𝑏 βˆͺ {𝑐})𝑧 ≀ 𝑦))
1512, 14imbi12d 343 . . . 4 (π‘Ž = (𝑏 βˆͺ {𝑐}) β†’ (((𝐾 ∈ Dirset ∧ π‘Ž βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ π‘Ž 𝑧 ≀ 𝑦) ↔ ((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ (𝑏 βˆͺ {𝑐})𝑧 ≀ 𝑦)))
16 sseq1 4006 . . . . . 6 (π‘Ž = 𝑋 β†’ (π‘Ž βŠ† 𝐡 ↔ 𝑋 βŠ† 𝐡))
1716anbi2d 627 . . . . 5 (π‘Ž = 𝑋 β†’ ((𝐾 ∈ Dirset ∧ π‘Ž βŠ† 𝐡) ↔ (𝐾 ∈ Dirset ∧ 𝑋 βŠ† 𝐡)))
18 raleq 3320 . . . . . 6 (π‘Ž = 𝑋 β†’ (βˆ€π‘§ ∈ π‘Ž 𝑧 ≀ 𝑦 ↔ βˆ€π‘§ ∈ 𝑋 𝑧 ≀ 𝑦))
1918rexbidv 3176 . . . . 5 (π‘Ž = 𝑋 β†’ (βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ π‘Ž 𝑧 ≀ 𝑦 ↔ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑋 𝑧 ≀ 𝑦))
2017, 19imbi12d 343 . . . 4 (π‘Ž = 𝑋 β†’ (((𝐾 ∈ Dirset ∧ π‘Ž βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ π‘Ž 𝑧 ≀ 𝑦) ↔ ((𝐾 ∈ Dirset ∧ 𝑋 βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑋 𝑧 ≀ 𝑦)))
21 drsbn0.b . . . . . . 7 𝐡 = (Baseβ€˜πΎ)
2221drsbn0 18261 . . . . . 6 (𝐾 ∈ Dirset β†’ 𝐡 β‰  βˆ…)
23 ral0 4511 . . . . . . . . 9 βˆ€π‘§ ∈ βˆ… 𝑧 ≀ 𝑦
2423jctr 523 . . . . . . . 8 (𝑦 ∈ 𝐡 β†’ (𝑦 ∈ 𝐡 ∧ βˆ€π‘§ ∈ βˆ… 𝑧 ≀ 𝑦))
2524eximi 1835 . . . . . . 7 (βˆƒπ‘¦ 𝑦 ∈ 𝐡 β†’ βˆƒπ‘¦(𝑦 ∈ 𝐡 ∧ βˆ€π‘§ ∈ βˆ… 𝑧 ≀ 𝑦))
26 n0 4345 . . . . . . 7 (𝐡 β‰  βˆ… ↔ βˆƒπ‘¦ 𝑦 ∈ 𝐡)
27 df-rex 3069 . . . . . . 7 (βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ βˆ… 𝑧 ≀ 𝑦 ↔ βˆƒπ‘¦(𝑦 ∈ 𝐡 ∧ βˆ€π‘§ ∈ βˆ… 𝑧 ≀ 𝑦))
2825, 26, 273imtr4i 291 . . . . . 6 (𝐡 β‰  βˆ… β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ βˆ… 𝑧 ≀ 𝑦)
2922, 28syl 17 . . . . 5 (𝐾 ∈ Dirset β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ βˆ… 𝑧 ≀ 𝑦)
3029adantr 479 . . . 4 ((𝐾 ∈ Dirset ∧ βˆ… βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ βˆ… 𝑧 ≀ 𝑦)
31 ssun1 4171 . . . . . . . . 9 𝑏 βŠ† (𝑏 βˆͺ {𝑐})
32 sstr 3989 . . . . . . . . 9 ((𝑏 βŠ† (𝑏 βˆͺ {𝑐}) ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) β†’ 𝑏 βŠ† 𝐡)
3331, 32mpan 686 . . . . . . . 8 ((𝑏 βˆͺ {𝑐}) βŠ† 𝐡 β†’ 𝑏 βŠ† 𝐡)
3433anim2i 615 . . . . . . 7 ((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) β†’ (𝐾 ∈ Dirset ∧ 𝑏 βŠ† 𝐡))
35 breq2 5151 . . . . . . . . . 10 (𝑦 = π‘Ž β†’ (𝑧 ≀ 𝑦 ↔ 𝑧 ≀ π‘Ž))
3635ralbidv 3175 . . . . . . . . 9 (𝑦 = π‘Ž β†’ (βˆ€π‘§ ∈ 𝑏 𝑧 ≀ 𝑦 ↔ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž))
3736cbvrexvw 3233 . . . . . . . 8 (βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑏 𝑧 ≀ 𝑦 ↔ βˆƒπ‘Ž ∈ 𝐡 βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)
38 simplrr 774 . . . . . . . . . . . 12 ((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ (π‘Ž ∈ 𝐡 ∧ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) β†’ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)
39 drsprs 18260 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ Dirset β†’ 𝐾 ∈ Proset )
4039ad5antr 730 . . . . . . . . . . . . . . . 16 ((((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) ∧ 𝑧 ∈ 𝑏) ∧ 𝑧 ≀ π‘Ž) β†’ 𝐾 ∈ Proset )
4133ad2antlr 723 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) β†’ 𝑏 βŠ† 𝐡)
4241adantr 479 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) β†’ 𝑏 βŠ† 𝐡)
4342sselda 3981 . . . . . . . . . . . . . . . . 17 (((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) ∧ 𝑧 ∈ 𝑏) β†’ 𝑧 ∈ 𝐡)
4443adantr 479 . . . . . . . . . . . . . . . 16 ((((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) ∧ 𝑧 ∈ 𝑏) ∧ 𝑧 ≀ π‘Ž) β†’ 𝑧 ∈ 𝐡)
45 simp-4r 780 . . . . . . . . . . . . . . . 16 ((((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) ∧ 𝑧 ∈ 𝑏) ∧ 𝑧 ≀ π‘Ž) β†’ π‘Ž ∈ 𝐡)
46 simprl 767 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) β†’ 𝑦 ∈ 𝐡)
4746ad2antrr 722 . . . . . . . . . . . . . . . 16 ((((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) ∧ 𝑧 ∈ 𝑏) ∧ 𝑧 ≀ π‘Ž) β†’ 𝑦 ∈ 𝐡)
48 simpr 483 . . . . . . . . . . . . . . . 16 ((((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) ∧ 𝑧 ∈ 𝑏) ∧ 𝑧 ≀ π‘Ž) β†’ 𝑧 ≀ π‘Ž)
49 simprrl 777 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) β†’ π‘Ž ≀ 𝑦)
5049ad2antrr 722 . . . . . . . . . . . . . . . 16 ((((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) ∧ 𝑧 ∈ 𝑏) ∧ 𝑧 ≀ π‘Ž) β†’ π‘Ž ≀ 𝑦)
51 drsdirfi.l . . . . . . . . . . . . . . . . 17 ≀ = (leβ€˜πΎ)
5221, 51prstr 18257 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Proset ∧ (𝑧 ∈ 𝐡 ∧ π‘Ž ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ (𝑧 ≀ π‘Ž ∧ π‘Ž ≀ 𝑦)) β†’ 𝑧 ≀ 𝑦)
5340, 44, 45, 47, 48, 50, 52syl132anc 1386 . . . . . . . . . . . . . . 15 ((((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) ∧ 𝑧 ∈ 𝑏) ∧ 𝑧 ≀ π‘Ž) β†’ 𝑧 ≀ 𝑦)
5453ex 411 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) ∧ 𝑧 ∈ 𝑏) β†’ (𝑧 ≀ π‘Ž β†’ 𝑧 ≀ 𝑦))
5554ralimdva 3165 . . . . . . . . . . . . 13 ((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) β†’ (βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž β†’ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ 𝑦))
5655adantlrr 717 . . . . . . . . . . . 12 ((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ (π‘Ž ∈ 𝐡 ∧ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) β†’ (βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž β†’ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ 𝑦))
5738, 56mpd 15 . . . . . . . . . . 11 ((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ (π‘Ž ∈ 𝐡 ∧ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) β†’ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ 𝑦)
58 simprrr 778 . . . . . . . . . . . 12 ((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ (π‘Ž ∈ 𝐡 ∧ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) β†’ 𝑐 ≀ 𝑦)
59 vex 3476 . . . . . . . . . . . . 13 𝑐 ∈ V
60 breq1 5150 . . . . . . . . . . . . 13 (𝑧 = 𝑐 β†’ (𝑧 ≀ 𝑦 ↔ 𝑐 ≀ 𝑦))
6159, 60ralsn 4684 . . . . . . . . . . . 12 (βˆ€π‘§ ∈ {𝑐}𝑧 ≀ 𝑦 ↔ 𝑐 ≀ 𝑦)
6258, 61sylibr 233 . . . . . . . . . . 11 ((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ (π‘Ž ∈ 𝐡 ∧ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) β†’ βˆ€π‘§ ∈ {𝑐}𝑧 ≀ 𝑦)
63 ralun 4191 . . . . . . . . . . 11 ((βˆ€π‘§ ∈ 𝑏 𝑧 ≀ 𝑦 ∧ βˆ€π‘§ ∈ {𝑐}𝑧 ≀ 𝑦) β†’ βˆ€π‘§ ∈ (𝑏 βˆͺ {𝑐})𝑧 ≀ 𝑦)
6457, 62, 63syl2anc 582 . . . . . . . . . 10 ((((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ (π‘Ž ∈ 𝐡 ∧ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)) ∧ (𝑦 ∈ 𝐡 ∧ (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))) β†’ βˆ€π‘§ ∈ (𝑏 βˆͺ {𝑐})𝑧 ≀ 𝑦)
65 simpll 763 . . . . . . . . . . 11 (((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ (π‘Ž ∈ 𝐡 ∧ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)) β†’ 𝐾 ∈ Dirset)
66 simprl 767 . . . . . . . . . . 11 (((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ (π‘Ž ∈ 𝐡 ∧ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)) β†’ π‘Ž ∈ 𝐡)
67 ssun2 4172 . . . . . . . . . . . . . 14 {𝑐} βŠ† (𝑏 βˆͺ {𝑐})
68 sstr 3989 . . . . . . . . . . . . . 14 (({𝑐} βŠ† (𝑏 βˆͺ {𝑐}) ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) β†’ {𝑐} βŠ† 𝐡)
6967, 68mpan 686 . . . . . . . . . . . . 13 ((𝑏 βˆͺ {𝑐}) βŠ† 𝐡 β†’ {𝑐} βŠ† 𝐡)
7059snss 4788 . . . . . . . . . . . . 13 (𝑐 ∈ 𝐡 ↔ {𝑐} βŠ† 𝐡)
7169, 70sylibr 233 . . . . . . . . . . . 12 ((𝑏 βˆͺ {𝑐}) βŠ† 𝐡 β†’ 𝑐 ∈ 𝐡)
7271ad2antlr 723 . . . . . . . . . . 11 (((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ (π‘Ž ∈ 𝐡 ∧ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)) β†’ 𝑐 ∈ 𝐡)
7321, 51drsdir 18259 . . . . . . . . . . 11 ((𝐾 ∈ Dirset ∧ π‘Ž ∈ 𝐡 ∧ 𝑐 ∈ 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))
7465, 66, 72, 73syl3anc 1369 . . . . . . . . . 10 (((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ (π‘Ž ∈ 𝐡 ∧ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)) β†’ βˆƒπ‘¦ ∈ 𝐡 (π‘Ž ≀ 𝑦 ∧ 𝑐 ≀ 𝑦))
7564, 74reximddv 3169 . . . . . . . . 9 (((𝐾 ∈ Dirset ∧ (𝑏 βˆͺ {𝑐}) βŠ† 𝐡) ∧ (π‘Ž ∈ 𝐡 ∧ βˆ€π‘§ ∈ 𝑏 𝑧 ≀ π‘Ž)) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ (𝑏 βˆͺ {𝑐})𝑧 ≀ 𝑦)
7675rexlimdvaa 3154 . . . . . . . 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 9166 . . 3 (𝑋 ∈ Fin β†’ ((𝐾 ∈ Dirset ∧ 𝑋 βŠ† 𝐡) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑋 𝑧 ≀ 𝑦))
8281com12 32 . 2 ((𝐾 ∈ Dirset ∧ 𝑋 βŠ† 𝐡) β†’ (𝑋 ∈ Fin β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑋 𝑧 ≀ 𝑦))
83823impia 1115 1 ((𝐾 ∈ Dirset ∧ 𝑋 βŠ† 𝐡 ∧ 𝑋 ∈ Fin) β†’ βˆƒπ‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝑋 𝑧 ≀ 𝑦)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 394   ∧ w3a 1085   = wceq 1539  βˆƒwex 1779   ∈ wcel 2104   β‰  wne 2938  βˆ€wral 3059  βˆƒwrex 3068   βˆͺ cun 3945   βŠ† wss 3947  βˆ…c0 4321  {csn 4627   class class class wbr 5147  β€˜cfv 6542  Fincfn 8941  Basecbs 17148  lecple 17208   Proset cproset 18250  Dirsetcdrs 18251
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-om 7858  df-en 8942  df-fin 8945  df-proset 18252  df-drs 18253
This theorem is referenced by:  isdrs2  18263  ipodrsfi  18496
  Copyright terms: Public domain W3C validator