Metamath Proof Explorer

Theorem tailf

Description: The tail function of a directed set sends its elements to its subsets. (Contributed by Jeff Hankins, 25-Nov-2009) (Revised by Mario Carneiro, 24-Nov-2013)

Ref Expression
Hypothesis tailf.1 ⊢ X = dom ⁡ D
Assertion tailf ⊢ D ∈ DirRel → tail ⁡ D : X ⟶ 𝒫 X

Proof

Step Hyp Ref Expression
1 tailf.1 ⊢ X = dom ⁡ D
2 imassrn ⊢ D x ⊆ ran ⁡ D
3 ssun2 ⊢ ran ⁡ D ⊆ dom ⁡ D ∪ ran ⁡ D
4 dmrnssfld ⊢ dom ⁡ D ∪ ran ⁡ D ⊆ ⋃ ⋃ D
5 3 4 sstri ⊢ ran ⁡ D ⊆ ⋃ ⋃ D
6 2 5 sstri ⊢ D x ⊆ ⋃ ⋃ D
7 dirdm ⊢ D ∈ DirRel → dom ⁡ D = ⋃ ⋃ D
8 1 7 syl5req ⊢ D ∈ DirRel → ⋃ ⋃ D = X
9 6 8 sseqtrid ⊢ D ∈ DirRel → D x ⊆ X
10 dmexg ⊢ D ∈ DirRel → dom ⁡ D ∈ V
11 1 10 eqeltrid ⊢ D ∈ DirRel → X ∈ V
12 elpw2g ⊢ X ∈ V → D x ∈ 𝒫 X ↔ D x ⊆ X
13 11 12 syl ⊢ D ∈ DirRel → D x ∈ 𝒫 X ↔ D x ⊆ X
14 9 13 mpbird ⊢ D ∈ DirRel → D x ∈ 𝒫 X
15 14 ralrimivw ⊢ D ∈ DirRel → ∀ x ∈ X D x ∈ 𝒫 X
16 eqid ⊢ x ∈ X ⟼ D x = x ∈ X ⟼ D x
17 16 fmpt ⊢ ∀ x ∈ X D x ∈ 𝒫 X ↔ x ∈ X ⟼ D x : X ⟶ 𝒫 X
18 15 17 sylib ⊢ D ∈ DirRel → x ∈ X ⟼ D x : X ⟶ 𝒫 X
19 1 tailfval ⊢ D ∈ DirRel → tail ⁡ D = x ∈ X ⟼ D x
20 19 feq1d ⊢ D ∈ DirRel → tail ⁡ D : X ⟶ 𝒫 X ↔ x ∈ X ⟼ D x : X ⟶ 𝒫 X
21 18 20 mpbird ⊢ D ∈ DirRel → tail ⁡ D : X ⟶ 𝒫 X