fmid

Description: The filter map applied to the identity. (Contributed by Jeff Hankins, 8-Nov-2009) (Revised by Mario Carneiro, 27-Aug-2015)

		Ref	Expression
	Assertion	fmid	$⊢ F \in Fil (X) \to (X FilMap ({I ↾}_{X})) (F) = F$

Proof

Step	Hyp	Ref	Expression
1		filfbas	$⊢ F \in Fil (X) \to F \in fBas (X)$
2		f1oi	$⊢ ({I ↾}_{X}) : X \underset{1-1 onto}{⟶} X$
3		f1ofo	$⊢ ({I ↾}_{X}) : X \underset{1-1 onto}{⟶} X \to ({I ↾}_{X}) : X \underset{onto}{⟶} X$
4	2 3	ax-mp	$⊢ ({I ↾}_{X}) : X \underset{onto}{⟶} X$
5		eqid	$⊢ X filGen F = X filGen F$
6	5	elfm3	$⊢ (F \in fBas (X) \land ({I ↾}_{X}) : X \underset{onto}{⟶} X) \to (t \in (X FilMap ({I ↾}_{X})) (F) \leftrightarrow \exists s \in (X filGen F) t = ({I ↾}_{X}) [s])$
7	1 4 6	sylancl	$⊢ F \in Fil (X) \to (t \in (X FilMap ({I ↾}_{X})) (F) \leftrightarrow \exists s \in (X filGen F) t = ({I ↾}_{X}) [s])$
8		fgfil	$⊢ F \in Fil (X) \to X filGen F = F$
9	8	rexeqdv	$⊢ F \in Fil (X) \to (\exists s \in (X filGen F) t = ({I ↾}_{X}) [s] \leftrightarrow \exists s \in F t = ({I ↾}_{X}) [s])$
10		filelss	$⊢ (F \in Fil (X) \land s \in F) \to s \subseteq X$
11		resiima	$⊢ s \subseteq X \to ({I ↾}_{X}) [s] = s$
12	10 11	syl	$⊢ (F \in Fil (X) \land s \in F) \to ({I ↾}_{X}) [s] = s$
13	12	eqeq2d	$⊢ (F \in Fil (X) \land s \in F) \to (t = ({I ↾}_{X}) [s] \leftrightarrow t = s)$
14		equcom	$⊢ s = t \leftrightarrow t = s$
15	13 14	bitr4di	$⊢ (F \in Fil (X) \land s \in F) \to (t = ({I ↾}_{X}) [s] \leftrightarrow s = t)$
16	15	rexbidva	$⊢ F \in Fil (X) \to (\exists s \in F t = ({I ↾}_{X}) [s] \leftrightarrow \exists s \in F s = t)$
17		risset	$⊢ t \in F \leftrightarrow \exists s \in F s = t$
18	16 17	bitr4di	$⊢ F \in Fil (X) \to (\exists s \in F t = ({I ↾}_{X}) [s] \leftrightarrow t \in F)$
19	7 9 18	3bitrd	$⊢ F \in Fil (X) \to (t \in (X FilMap ({I ↾}_{X})) (F) \leftrightarrow t \in F)$
20	19	eqrdv	$⊢ F \in Fil (X) \to (X FilMap ({I ↾}_{X})) (F) = F$

Metamath Proof Explorer

Theorem fmid

Proof