This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isdrs2

Description: Directed sets may be defined in terms of finite subsets. Again, without nonemptiness we would need to restrict to nonempty subsets here. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Hypotheses drsbn0.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
drsdirfi.l ⊢ ≤ = ( le ‘ 𝐾 )
Assertion isdrs2 ( 𝐾 ∈ Dirset ↔ ( 𝐾 ∈ Proset ∧ ∀ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ) )

Proof

Step Hyp Ref Expression
1 drsbn0.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 drsdirfi.l ⊢ ≤ = ( le ‘ 𝐾 )
3 drsprs ⊢ ( 𝐾 ∈ Dirset → 𝐾 ∈ Proset )
4 simpl ⊢ ( ( 𝐾 ∈ Dirset ∧ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝐾 ∈ Dirset )
5 elinel1 ⊢ ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) → 𝑥 ∈ 𝒫 𝐵 )
6 5 elpwid ⊢ ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) → 𝑥 ⊆ 𝐵 )
7 6 adantl ⊢ ( ( 𝐾 ∈ Dirset ∧ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝑥 ⊆ 𝐵 )
8 elinel2 ⊢ ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) → 𝑥 ∈ Fin )
9 8 adantl ⊢ ( ( 𝐾 ∈ Dirset ∧ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝑥 ∈ Fin )
10 1 2 drsdirfi ⊢ ( ( 𝐾 ∈ Dirset ∧ 𝑥 ⊆ 𝐵 ∧ 𝑥 ∈ Fin ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 )
11 4 7 9 10 syl3anc ⊢ ( ( 𝐾 ∈ Dirset ∧ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 )
12 11 ralrimiva ⊢ ( 𝐾 ∈ Dirset → ∀ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 )
13 3 12 jca ⊢ ( 𝐾 ∈ Dirset → ( 𝐾 ∈ Proset ∧ ∀ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ) )
14 simpl ⊢ ( ( 𝐾 ∈ Proset ∧ ∀ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ) → 𝐾 ∈ Proset )
15 0elpw ⊢ ∅ ∈ 𝒫 𝐵
16 0fi ⊢ ∅ ∈ Fin
17 15 16 elini ⊢ ∅ ∈ ( 𝒫 𝐵 ∩ Fin )
18 raleq ⊢ ( 𝑥 = ∅ → ( ∀ 𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ↔ ∀ 𝑧 ∈ ∅ 𝑧 ≤ 𝑦 ) )
19 18 rexbidv ⊢ ( 𝑥 = ∅ → ( ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ↔ ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ∅ 𝑧 ≤ 𝑦 ) )
20 19 rspcv ⊢ ( ∅ ∈ ( 𝒫 𝐵 ∩ Fin ) → ( ∀ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ∅ 𝑧 ≤ 𝑦 ) )
21 17 20 ax-mp ⊢ ( ∀ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ∅ 𝑧 ≤ 𝑦 )
22 rexn0 ⊢ ( ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ∅ 𝑧 ≤ 𝑦 → 𝐵 ≠ ∅ )
23 21 22 syl ⊢ ( ∀ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 → 𝐵 ≠ ∅ )
24 23 adantl ⊢ ( ( 𝐾 ∈ Proset ∧ ∀ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ) → 𝐵 ≠ ∅ )
25 raleq ⊢ ( 𝑥 = { 𝑎 , 𝑏 } → ( ∀ 𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ↔ ∀ 𝑧 ∈ { 𝑎 , 𝑏 } 𝑧 ≤ 𝑦 ) )
26 25 rexbidv ⊢ ( 𝑥 = { 𝑎 , 𝑏 } → ( ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ↔ ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ { 𝑎 , 𝑏 } 𝑧 ≤ 𝑦 ) )
27 simplr ⊢ ( ( ( 𝐾 ∈ Proset ∧ ∀ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 )
28 prelpwi ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → { 𝑎 , 𝑏 } ∈ 𝒫 𝐵 )
29 prfi ⊢ { 𝑎 , 𝑏 } ∈ Fin
30 29 a1i ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → { 𝑎 , 𝑏 } ∈ Fin )
31 28 30 elind ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → { 𝑎 , 𝑏 } ∈ ( 𝒫 𝐵 ∩ Fin ) )
32 31 adantl ⊢ ( ( ( 𝐾 ∈ Proset ∧ ∀ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → { 𝑎 , 𝑏 } ∈ ( 𝒫 𝐵 ∩ Fin ) )
33 26 27 32 rspcdva ⊢ ( ( ( 𝐾 ∈ Proset ∧ ∀ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ { 𝑎 , 𝑏 } 𝑧 ≤ 𝑦 )
34 vex ⊢ 𝑎 ∈ V
35 vex ⊢ 𝑏 ∈ V
36 breq1 ⊢ ( 𝑧 = 𝑎 → ( 𝑧 ≤ 𝑦 ↔ 𝑎 ≤ 𝑦 ) )
37 breq1 ⊢ ( 𝑧 = 𝑏 → ( 𝑧 ≤ 𝑦 ↔ 𝑏 ≤ 𝑦 ) )
38 34 35 36 37 ralpr ⊢ ( ∀ 𝑧 ∈ { 𝑎 , 𝑏 } 𝑧 ≤ 𝑦 ↔ ( 𝑎 ≤ 𝑦 ∧ 𝑏 ≤ 𝑦 ) )
39 38 rexbii ⊢ ( ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ { 𝑎 , 𝑏 } 𝑧 ≤ 𝑦 ↔ ∃ 𝑦 ∈ 𝐵 ( 𝑎 ≤ 𝑦 ∧ 𝑏 ≤ 𝑦 ) )
40 33 39 sylib ⊢ ( ( ( 𝐾 ∈ Proset ∧ ∀ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ∃ 𝑦 ∈ 𝐵 ( 𝑎 ≤ 𝑦 ∧ 𝑏 ≤ 𝑦 ) )
41 40 ralrimivva ⊢ ( ( 𝐾 ∈ Proset ∧ ∀ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ) → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( 𝑎 ≤ 𝑦 ∧ 𝑏 ≤ 𝑦 ) )
42 1 2 isdrs ⊢ ( 𝐾 ∈ Dirset ↔ ( 𝐾 ∈ Proset ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( 𝑎 ≤ 𝑦 ∧ 𝑏 ≤ 𝑦 ) ) )
43 14 24 41 42 syl3anbrc ⊢ ( ( 𝐾 ∈ Proset ∧ ∀ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ) → 𝐾 ∈ Dirset )
44 13 43 impbii ⊢ ( 𝐾 ∈ Dirset ↔ ( 𝐾 ∈ Proset ∧ ∀ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ) )