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 \in DirRel \to tail (D) : X ⟶ 𝒫 X$

Proof

Step	Hyp	Ref	Expression
1		tailf.1	$⊢ X = dom D$
2		imassrn	$⊢ D [\{x\}] \subseteq ran D$
3		ssun2	$⊢ ran D \subseteq dom D \cup ran D$
4		dmrnssfld	$⊢ dom D \cup ran D \subseteq ⋃ ⋃ D$
5	3 4	sstri	$⊢ ran D \subseteq ⋃ ⋃ D$
6	2 5	sstri	$⊢ D [\{x\}] \subseteq ⋃ ⋃ D$
7		dirdm	$⊢ D \in DirRel \to dom D = ⋃ ⋃ D$
8	1 7	eqtr2id	$⊢ D \in DirRel \to ⋃ ⋃ D = X$
9	6 8	sseqtrid	$⊢ D \in DirRel \to D [\{x\}] \subseteq X$
10		dmexg	$⊢ D \in DirRel \to dom D \in V$
11	1 10	eqeltrid	$⊢ D \in DirRel \to X \in V$
12		elpw2g	$⊢ X \in V \to (D [\{x\}] \in 𝒫 X \leftrightarrow D [\{x\}] \subseteq X)$
13	11 12	syl	$⊢ D \in DirRel \to (D [\{x\}] \in 𝒫 X \leftrightarrow D [\{x\}] \subseteq X)$
14	9 13	mpbird	$⊢ D \in DirRel \to D [\{x\}] \in 𝒫 X$
15	14	ralrimivw	$⊢ D \in DirRel \to \forall x \in X D [\{x\}] \in 𝒫 X$
16		eqid	$⊢ (x \in X ⟼ D [\{x\}]) = (x \in X ⟼ D [\{x\}])$
17	16	fmpt	$⊢ \forall x \in X D [\{x\}] \in 𝒫 X \leftrightarrow (x \in X ⟼ D [\{x\}]) : X ⟶ 𝒫 X$
18	15 17	sylib	$⊢ D \in DirRel \to (x \in X ⟼ D [\{x\}]) : X ⟶ 𝒫 X$
19	1	tailfval	$⊢ D \in DirRel \to tail (D) = (x \in X ⟼ D [\{x\}])$
20	19	feq1d	$⊢ D \in DirRel \to (tail (D) : X ⟶ 𝒫 X \leftrightarrow (x \in X ⟼ D [\{x\}]) : X ⟶ 𝒫 X)$
21	18 20	mpbird	$⊢ D \in DirRel \to tail (D) : X ⟶ 𝒫 X$

Metamath Proof Explorer

Theorem tailf

Proof