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 0fin ∅ ∈ 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 ) ∃ 𝑦𝐵𝑧𝑥 𝑧 𝑦 ) )