isdrs

Description: Property of being a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Hypotheses	isdrs.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	isdrs.l	⊢ ≤ = ( le ‘ 𝐾 )
Assertion	isdrs	⊢ ( 𝐾 ∈ Dirset ↔ ( 𝐾 ∈ Proset ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isdrs.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		isdrs.l	⊢ ≤ = ( le ‘ 𝐾 )
3		fveq2	⊢ ( 𝑓 = 𝐾 → ( Base ‘ 𝑓 ) = ( Base ‘ 𝐾 ) )
4	3 1	eqtr4di	⊢ ( 𝑓 = 𝐾 → ( Base ‘ 𝑓 ) = 𝐵 )
5		fveq2	⊢ ( 𝑓 = 𝐾 → ( le ‘ 𝑓 ) = ( le ‘ 𝐾 ) )
6	5 2	eqtr4di	⊢ ( 𝑓 = 𝐾 → ( le ‘ 𝑓 ) = ≤ )
7	6	sbceq1d	⊢ ( 𝑓 = 𝐾 → ( [ ( le ‘ 𝑓 ) / 𝑟 ] ( 𝑏 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ) ↔ [ ≤ / 𝑟 ] ( 𝑏 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ) ) )
8	4 7	sbceqbid	⊢ ( 𝑓 = 𝐾 → ( [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ( 𝑏 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ) ↔ [ 𝐵 / 𝑏 ] [ ≤ / 𝑟 ] ( 𝑏 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ) ) )
9	1	fvexi	⊢ 𝐵 ∈ V
10	2	fvexi	⊢ ≤ ∈ V
11		neeq1	⊢ ( 𝑏 = 𝐵 → ( 𝑏 ≠ ∅ ↔ 𝐵 ≠ ∅ ) )
12	11	adantr	⊢ ( ( 𝑏 = 𝐵 ∧ 𝑟 = ≤ ) → ( 𝑏 ≠ ∅ ↔ 𝐵 ≠ ∅ ) )
13		rexeq	⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ↔ ∃ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ) )
14	13	raleqbi1dv	⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ) )
15	14	raleqbi1dv	⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ) )
16		breq	⊢ ( 𝑟 = ≤ → ( 𝑥 𝑟 𝑧 ↔ 𝑥 ≤ 𝑧 ) )
17		breq	⊢ ( 𝑟 = ≤ → ( 𝑦 𝑟 𝑧 ↔ 𝑦 ≤ 𝑧 ) )
18	16 17	anbi12d	⊢ ( 𝑟 = ≤ → ( ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ↔ ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) )
19	18	rexbidv	⊢ ( 𝑟 = ≤ → ( ∃ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ↔ ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) )
20	19	2ralbidv	⊢ ( 𝑟 = ≤ → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) )
21	15 20	sylan9bb	⊢ ( ( 𝑏 = 𝐵 ∧ 𝑟 = ≤ ) → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) )
22	12 21	anbi12d	⊢ ( ( 𝑏 = 𝐵 ∧ 𝑟 = ≤ ) → ( ( 𝑏 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ) ↔ ( 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) ) )
23	9 10 22	sbc2ie	⊢ ( [ 𝐵 / 𝑏 ] [ ≤ / 𝑟 ] ( 𝑏 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ) ↔ ( 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) )
24	8 23	bitrdi	⊢ ( 𝑓 = 𝐾 → ( [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ( 𝑏 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ) ↔ ( 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) ) )
25		df-drs	⊢ Dirset = { 𝑓 ∈ Proset ∣ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ( 𝑏 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ) }
26	24 25	elrab2	⊢ ( 𝐾 ∈ Dirset ↔ ( 𝐾 ∈ Proset ∧ ( 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) ) )
27		3anass	⊢ ( ( 𝐾 ∈ Proset ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) ↔ ( 𝐾 ∈ Proset ∧ ( 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) ) )
28	26 27	bitr4i	⊢ ( 𝐾 ∈ Dirset ↔ ( 𝐾 ∈ Proset ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) )

Metamath Proof Explorer

Theorem isdrs

Proof