Metamath Proof Explorer

Theorem drsdirfi

Description: Anyfinite number of elements in a directed set have a common upper bound. Here is where the nonemptiness constraint in df-drs first comes into play; without it we would need an additional constraint that X not be empty. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Hypotheses drsbn0.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
drsdirfi.l ⊢ ≤ = ( le ‘ 𝐾 )
Assertion drsdirfi ( ( 𝐾 ∈ Dirset ∧ 𝑋 ⊆ 𝐵 ∧ 𝑋 ∈ Fin ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑋 𝑧 ≤ 𝑦 )

Proof

Step Hyp Ref Expression
1 drsbn0.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 drsdirfi.l ⊢ ≤ = ( le ‘ 𝐾 )
3 sseq1 ⊢ ( 𝑎 = ∅ → ( 𝑎 ⊆ 𝐵 ↔ ∅ ⊆ 𝐵 ) )
4 3 anbi2d ⊢ ( 𝑎 = ∅ → ( ( 𝐾 ∈ Dirset ∧ 𝑎 ⊆ 𝐵 ) ↔ ( 𝐾 ∈ Dirset ∧ ∅ ⊆ 𝐵 ) ) )
5 raleq ⊢ ( 𝑎 = ∅ → ( ∀ 𝑧 ∈ 𝑎 𝑧 ≤ 𝑦 ↔ ∀ 𝑧 ∈ ∅ 𝑧 ≤ 𝑦 ) )
6 5 rexbidv ⊢ ( 𝑎 = ∅ → ( ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑎 𝑧 ≤ 𝑦 ↔ ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ∅ 𝑧 ≤ 𝑦 ) )
7 4 6 imbi12d ⊢ ( 𝑎 = ∅ → ( ( ( 𝐾 ∈ Dirset ∧ 𝑎 ⊆ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑎 𝑧 ≤ 𝑦 ) ↔ ( ( 𝐾 ∈ Dirset ∧ ∅ ⊆ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ∅ 𝑧 ≤ 𝑦 ) ) )
8 sseq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑎 ⊆ 𝐵 ↔ 𝑏 ⊆ 𝐵 ) )
9 8 anbi2d ⊢ ( 𝑎 = 𝑏 → ( ( 𝐾 ∈ Dirset ∧ 𝑎 ⊆ 𝐵 ) ↔ ( 𝐾 ∈ Dirset ∧ 𝑏 ⊆ 𝐵 ) ) )
10 raleq ⊢ ( 𝑎 = 𝑏 → ( ∀ 𝑧 ∈ 𝑎 𝑧 ≤ 𝑦 ↔ ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑦 ) )
11 10 rexbidv ⊢ ( 𝑎 = 𝑏 → ( ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑎 𝑧 ≤ 𝑦 ↔ ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑦 ) )
12 9 11 imbi12d ⊢ ( 𝑎 = 𝑏 → ( ( ( 𝐾 ∈ Dirset ∧ 𝑎 ⊆ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑎 𝑧 ≤ 𝑦 ) ↔ ( ( 𝐾 ∈ Dirset ∧ 𝑏 ⊆ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑦 ) ) )
13 sseq1 ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( 𝑎 ⊆ 𝐵 ↔ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) )
14 13 anbi2d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ( 𝐾 ∈ Dirset ∧ 𝑎 ⊆ 𝐵 ) ↔ ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ) )
15 raleq ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ∀ 𝑧 ∈ 𝑎 𝑧 ≤ 𝑦 ↔ ∀ 𝑧 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝑧 ≤ 𝑦 ) )
16 15 rexbidv ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑎 𝑧 ≤ 𝑦 ↔ ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝑧 ≤ 𝑦 ) )
17 14 16 imbi12d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ( ( 𝐾 ∈ Dirset ∧ 𝑎 ⊆ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑎 𝑧 ≤ 𝑦 ) ↔ ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝑧 ≤ 𝑦 ) ) )
18 sseq1 ⊢ ( 𝑎 = 𝑋 → ( 𝑎 ⊆ 𝐵 ↔ 𝑋 ⊆ 𝐵 ) )
19 18 anbi2d ⊢ ( 𝑎 = 𝑋 → ( ( 𝐾 ∈ Dirset ∧ 𝑎 ⊆ 𝐵 ) ↔ ( 𝐾 ∈ Dirset ∧ 𝑋 ⊆ 𝐵 ) ) )
20 raleq ⊢ ( 𝑎 = 𝑋 → ( ∀ 𝑧 ∈ 𝑎 𝑧 ≤ 𝑦 ↔ ∀ 𝑧 ∈ 𝑋 𝑧 ≤ 𝑦 ) )
21 20 rexbidv ⊢ ( 𝑎 = 𝑋 → ( ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑎 𝑧 ≤ 𝑦 ↔ ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑋 𝑧 ≤ 𝑦 ) )
22 19 21 imbi12d ⊢ ( 𝑎 = 𝑋 → ( ( ( 𝐾 ∈ Dirset ∧ 𝑎 ⊆ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑎 𝑧 ≤ 𝑦 ) ↔ ( ( 𝐾 ∈ Dirset ∧ 𝑋 ⊆ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑋 𝑧 ≤ 𝑦 ) ) )
23 1 drsbn0 ⊢ ( 𝐾 ∈ Dirset → 𝐵 ≠ ∅ )
24 ral0 ⊢ ∀ 𝑧 ∈ ∅ 𝑧 ≤ 𝑦
25 24 jctr ⊢ ( 𝑦 ∈ 𝐵 → ( 𝑦 ∈ 𝐵 ∧ ∀ 𝑧 ∈ ∅ 𝑧 ≤ 𝑦 ) )
26 25 eximi ⊢ ( ∃ 𝑦 𝑦 ∈ 𝐵 → ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ∀ 𝑧 ∈ ∅ 𝑧 ≤ 𝑦 ) )
27 n0 ⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐵 )
28 df-rex ⊢ ( ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ∅ 𝑧 ≤ 𝑦 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ∀ 𝑧 ∈ ∅ 𝑧 ≤ 𝑦 ) )
29 26 27 28 3imtr4i ⊢ ( 𝐵 ≠ ∅ → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ∅ 𝑧 ≤ 𝑦 )
30 23 29 syl ⊢ ( 𝐾 ∈ Dirset → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ∅ 𝑧 ≤ 𝑦 )
31 30 adantr ⊢ ( ( 𝐾 ∈ Dirset ∧ ∅ ⊆ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ∅ 𝑧 ≤ 𝑦 )
32 ssun1 ⊢ 𝑏 ⊆ ( 𝑏 ∪ { 𝑐 } )
33 sstr ⊢ ( ( 𝑏 ⊆ ( 𝑏 ∪ { 𝑐 } ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) → 𝑏 ⊆ 𝐵 )
34 32 33 mpan ⊢ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 → 𝑏 ⊆ 𝐵 )
35 34 anim2i ⊢ ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) → ( 𝐾 ∈ Dirset ∧ 𝑏 ⊆ 𝐵 ) )
36 breq2 ⊢ ( 𝑦 = 𝑎 → ( 𝑧 ≤ 𝑦 ↔ 𝑧 ≤ 𝑎 ) )
37 36 ralbidv ⊢ ( 𝑦 = 𝑎 → ( ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑦 ↔ ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑎 ) )
38 37 cbvrexvw ⊢ ( ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑦 ↔ ∃ 𝑎 ∈ 𝐵 ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑎 )
39 simplrr ⊢ ( ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑎 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑎 ≤ 𝑦 ∧ 𝑐 ≤ 𝑦 ) ) ) → ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑎 )
40 drsprs ⊢ ( 𝐾 ∈ Dirset → 𝐾 ∈ Proset )
41 40 ad5antr ⊢ ( ( ( ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑎 ≤ 𝑦 ∧ 𝑐 ≤ 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑏 ) ∧ 𝑧 ≤ 𝑎 ) → 𝐾 ∈ Proset )
42 34 ad2antlr ⊢ ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) → 𝑏 ⊆ 𝐵 )
43 42 adantr ⊢ ( ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑎 ≤ 𝑦 ∧ 𝑐 ≤ 𝑦 ) ) ) → 𝑏 ⊆ 𝐵 )
44 43 sselda ⊢ ( ( ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑎 ≤ 𝑦 ∧ 𝑐 ≤ 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑏 ) → 𝑧 ∈ 𝐵 )
45 44 adantr ⊢ ( ( ( ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑎 ≤ 𝑦 ∧ 𝑐 ≤ 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑏 ) ∧ 𝑧 ≤ 𝑎 ) → 𝑧 ∈ 𝐵 )
46 simp-4r ⊢ ( ( ( ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑎 ≤ 𝑦 ∧ 𝑐 ≤ 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑏 ) ∧ 𝑧 ≤ 𝑎 ) → 𝑎 ∈ 𝐵 )
47 simprl ⊢ ( ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑎 ≤ 𝑦 ∧ 𝑐 ≤ 𝑦 ) ) ) → 𝑦 ∈ 𝐵 )
48 47 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑎 ≤ 𝑦 ∧ 𝑐 ≤ 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑏 ) ∧ 𝑧 ≤ 𝑎 ) → 𝑦 ∈ 𝐵 )
49 simpr ⊢ ( ( ( ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑎 ≤ 𝑦 ∧ 𝑐 ≤ 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑏 ) ∧ 𝑧 ≤ 𝑎 ) → 𝑧 ≤ 𝑎 )
50 simprrl ⊢ ( ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑎 ≤ 𝑦 ∧ 𝑐 ≤ 𝑦 ) ) ) → 𝑎 ≤ 𝑦 )
51 50 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑎 ≤ 𝑦 ∧ 𝑐 ≤ 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑏 ) ∧ 𝑧 ≤ 𝑎 ) → 𝑎 ≤ 𝑦 )
52 1 2 prstr ⊢ ( ( 𝐾 ∈ Proset ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ≤ 𝑎 ∧ 𝑎 ≤ 𝑦 ) ) → 𝑧 ≤ 𝑦 )
53 41 45 46 48 49 51 52 syl132anc ⊢ ( ( ( ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑎 ≤ 𝑦 ∧ 𝑐 ≤ 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑏 ) ∧ 𝑧 ≤ 𝑎 ) → 𝑧 ≤ 𝑦 )
54 53 ex ⊢ ( ( ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑎 ≤ 𝑦 ∧ 𝑐 ≤ 𝑦 ) ) ) ∧ 𝑧 ∈ 𝑏 ) → ( 𝑧 ≤ 𝑎 → 𝑧 ≤ 𝑦 ) )
55 54 ralimdva ⊢ ( ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑎 ≤ 𝑦 ∧ 𝑐 ≤ 𝑦 ) ) ) → ( ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑎 → ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑦 ) )
56 55 adantlrr ⊢ ( ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑎 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑎 ≤ 𝑦 ∧ 𝑐 ≤ 𝑦 ) ) ) → ( ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑎 → ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑦 ) )
57 39 56 mpd ⊢ ( ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑎 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑎 ≤ 𝑦 ∧ 𝑐 ≤ 𝑦 ) ) ) → ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑦 )
58 simprrr ⊢ ( ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑎 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑎 ≤ 𝑦 ∧ 𝑐 ≤ 𝑦 ) ) ) → 𝑐 ≤ 𝑦 )
59 vex ⊢ 𝑐 ∈ V
60 breq1 ⊢ ( 𝑧 = 𝑐 → ( 𝑧 ≤ 𝑦 ↔ 𝑐 ≤ 𝑦 ) )
61 59 60 ralsn ⊢ ( ∀ 𝑧 ∈ { 𝑐 } 𝑧 ≤ 𝑦 ↔ 𝑐 ≤ 𝑦 )
62 58 61 sylibr ⊢ ( ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑎 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑎 ≤ 𝑦 ∧ 𝑐 ≤ 𝑦 ) ) ) → ∀ 𝑧 ∈ { 𝑐 } 𝑧 ≤ 𝑦 )
63 ralun ⊢ ( ( ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑦 ∧ ∀ 𝑧 ∈ { 𝑐 } 𝑧 ≤ 𝑦 ) → ∀ 𝑧 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝑧 ≤ 𝑦 )
64 57 62 63 syl2anc ⊢ ( ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑎 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑎 ≤ 𝑦 ∧ 𝑐 ≤ 𝑦 ) ) ) → ∀ 𝑧 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝑧 ≤ 𝑦 )
65 simpll ⊢ ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑎 ) ) → 𝐾 ∈ Dirset )
66 simprl ⊢ ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑎 ) ) → 𝑎 ∈ 𝐵 )
67 ssun2 ⊢ { 𝑐 } ⊆ ( 𝑏 ∪ { 𝑐 } )
68 sstr ⊢ ( ( { 𝑐 } ⊆ ( 𝑏 ∪ { 𝑐 } ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) → { 𝑐 } ⊆ 𝐵 )
69 67 68 mpan ⊢ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 → { 𝑐 } ⊆ 𝐵 )
70 59 snss ⊢ ( 𝑐 ∈ 𝐵 ↔ { 𝑐 } ⊆ 𝐵 )
71 69 70 sylibr ⊢ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 → 𝑐 ∈ 𝐵 )
72 71 ad2antlr ⊢ ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑎 ) ) → 𝑐 ∈ 𝐵 )
73 1 2 drsdir ⊢ ( ( 𝐾 ∈ Dirset ∧ 𝑎 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑎 ≤ 𝑦 ∧ 𝑐 ≤ 𝑦 ) )
74 65 66 72 73 syl3anc ⊢ ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑎 ) ) → ∃ 𝑦 ∈ 𝐵 ( 𝑎 ≤ 𝑦 ∧ 𝑐 ≤ 𝑦 ) )
75 64 74 reximddv ⊢ ( ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑎 ) ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝑧 ≤ 𝑦 )
76 75 rexlimdvaa ⊢ ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) → ( ∃ 𝑎 ∈ 𝐵 ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑎 → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝑧 ≤ 𝑦 ) )
77 38 76 biimtrid ⊢ ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) → ( ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑦 → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝑧 ≤ 𝑦 ) )
78 35 77 embantd ⊢ ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) → ( ( ( 𝐾 ∈ Dirset ∧ 𝑏 ⊆ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑦 ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝑧 ≤ 𝑦 ) )
79 78 com12 ⊢ ( ( ( 𝐾 ∈ Dirset ∧ 𝑏 ⊆ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑦 ) → ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝑧 ≤ 𝑦 ) )
80 79 a1i ⊢ ( 𝑏 ∈ Fin → ( ( ( 𝐾 ∈ Dirset ∧ 𝑏 ⊆ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑏 𝑧 ≤ 𝑦 ) → ( ( 𝐾 ∈ Dirset ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝑧 ≤ 𝑦 ) ) )
81 7 12 17 22 31 80 findcard2 ⊢ ( 𝑋 ∈ Fin → ( ( 𝐾 ∈ Dirset ∧ 𝑋 ⊆ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑋 𝑧 ≤ 𝑦 ) )
82 81 com12 ⊢ ( ( 𝐾 ∈ Dirset ∧ 𝑋 ⊆ 𝐵 ) → ( 𝑋 ∈ Fin → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑋 𝑧 ≤ 𝑦 ) )
83 82 3impia ⊢ ( ( 𝐾 ∈ Dirset ∧ 𝑋 ⊆ 𝐵 ∧ 𝑋 ∈ Fin ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑋 𝑧 ≤ 𝑦 )