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 ) ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ) )