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 e. DirRel -> ( tail ` D ) : X --> ~P X )

Proof

Step	Hyp	Ref	Expression
1		tailf.1	|- X = dom D
2		imassrn	|- ( D " { x } ) C_ ran D
3		ssun2	|- ran D C_ ( dom D u. ran D )
4		dmrnssfld	|- ( dom D u. ran D ) C_ U. U. D
5	3 4	sstri	|- ran D C_ U. U. D
6	2 5	sstri	|- ( D " { x } ) C_ U. U. D
7		dirdm	|- ( D e. DirRel -> dom D = U. U. D )
8	1 7	syl5req	|- ( D e. DirRel -> U. U. D = X )
9	6 8	sseqtrid	|- ( D e. DirRel -> ( D " { x } ) C_ X )
10		dmexg	|- ( D e. DirRel -> dom D e. _V )
11	1 10	eqeltrid	|- ( D e. DirRel -> X e. _V )
12		elpw2g	|- ( X e. _V -> ( ( D " { x } ) e. ~P X <-> ( D " { x } ) C_ X ) )
13	11 12	syl	|- ( D e. DirRel -> ( ( D " { x } ) e. ~P X <-> ( D " { x } ) C_ X ) )
14	9 13	mpbird	|- ( D e. DirRel -> ( D " { x } ) e. ~P X )
15	14	ralrimivw	|- ( D e. DirRel -> A. x e. X ( D " { x } ) e. ~P X )
16		eqid	|- ( x e. X |-> ( D " { x } ) ) = ( x e. X |-> ( D " { x } ) )
17	16	fmpt	|- ( A. x e. X ( D " { x } ) e. ~P X <-> ( x e. X |-> ( D " { x } ) ) : X --> ~P X )
18	15 17	sylib	|- ( D e. DirRel -> ( x e. X |-> ( D " { x } ) ) : X --> ~P X )
19	1	tailfval	|- ( D e. DirRel -> ( tail ` D ) = ( x e. X |-> ( D " { x } ) ) )
20	19	feq1d	|- ( D e. DirRel -> ( ( tail ` D ) : X --> ~P X <-> ( x e. X |-> ( D " { x } ) ) : X --> ~P X ) )
21	18 20	mpbird	|- ( D e. DirRel -> ( tail ` D ) : X --> ~P X )