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	⊢ 𝑋 = dom 𝐷
Assertion	tailf	⊢ ( 𝐷 ∈ DirRel → ( tail ‘ 𝐷 ) : 𝑋 ⟶ 𝒫 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		tailf.1	⊢ 𝑋 = dom 𝐷
2		imassrn	⊢ ( 𝐷 “ { 𝑥 } ) ⊆ ran 𝐷
3		ssun2	⊢ ran 𝐷 ⊆ ( dom 𝐷 ∪ ran 𝐷 )
4		dmrnssfld	⊢ ( dom 𝐷 ∪ ran 𝐷 ) ⊆ ∪ ∪ 𝐷
5	3 4	sstri	⊢ ran 𝐷 ⊆ ∪ ∪ 𝐷
6	2 5	sstri	⊢ ( 𝐷 “ { 𝑥 } ) ⊆ ∪ ∪ 𝐷
7		dirdm	⊢ ( 𝐷 ∈ DirRel → dom 𝐷 = ∪ ∪ 𝐷 )
8	1 7	syl5req	⊢ ( 𝐷 ∈ DirRel → ∪ ∪ 𝐷 = 𝑋 )
9	6 8	sseqtrid	⊢ ( 𝐷 ∈ DirRel → ( 𝐷 “ { 𝑥 } ) ⊆ 𝑋 )
10		dmexg	⊢ ( 𝐷 ∈ DirRel → dom 𝐷 ∈ V )
11	1 10	eqeltrid	⊢ ( 𝐷 ∈ DirRel → 𝑋 ∈ V )
12		elpw2g	⊢ ( 𝑋 ∈ V → ( ( 𝐷 “ { 𝑥 } ) ∈ 𝒫 𝑋 ↔ ( 𝐷 “ { 𝑥 } ) ⊆ 𝑋 ) )
13	11 12	syl	⊢ ( 𝐷 ∈ DirRel → ( ( 𝐷 “ { 𝑥 } ) ∈ 𝒫 𝑋 ↔ ( 𝐷 “ { 𝑥 } ) ⊆ 𝑋 ) )
14	9 13	mpbird	⊢ ( 𝐷 ∈ DirRel → ( 𝐷 “ { 𝑥 } ) ∈ 𝒫 𝑋 )
15	14	ralrimivw	⊢ ( 𝐷 ∈ DirRel → ∀ 𝑥 ∈ 𝑋 ( 𝐷 “ { 𝑥 } ) ∈ 𝒫 𝑋 )
16		eqid	⊢ ( 𝑥 ∈ 𝑋 ↦ ( 𝐷 “ { 𝑥 } ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐷 “ { 𝑥 } ) )
17	16	fmpt	⊢ ( ∀ 𝑥 ∈ 𝑋 ( 𝐷 “ { 𝑥 } ) ∈ 𝒫 𝑋 ↔ ( 𝑥 ∈ 𝑋 ↦ ( 𝐷 “ { 𝑥 } ) ) : 𝑋 ⟶ 𝒫 𝑋 )
18	15 17	sylib	⊢ ( 𝐷 ∈ DirRel → ( 𝑥 ∈ 𝑋 ↦ ( 𝐷 “ { 𝑥 } ) ) : 𝑋 ⟶ 𝒫 𝑋 )
19	1	tailfval	⊢ ( 𝐷 ∈ DirRel → ( tail ‘ 𝐷 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐷 “ { 𝑥 } ) ) )
20	19	feq1d	⊢ ( 𝐷 ∈ DirRel → ( ( tail ‘ 𝐷 ) : 𝑋 ⟶ 𝒫 𝑋 ↔ ( 𝑥 ∈ 𝑋 ↦ ( 𝐷 “ { 𝑥 } ) ) : 𝑋 ⟶ 𝒫 𝑋 ) )
21	18 20	mpbird	⊢ ( 𝐷 ∈ DirRel → ( tail ‘ 𝐷 ) : 𝑋 ⟶ 𝒫 𝑋 )