fmufil

Description: An image filter of an ultrafilter is an ultrafilter. (Contributed by Jeff Hankins, 11-Dec-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

		Ref	Expression
	Assertion	fmufil	$⊢ (X \in A \land L \in UFil (Y) \land F : Y ⟶ X) \to (X FilMap F) (L) \in UFil (X)$

Proof

Step	Hyp	Ref	Expression
1		ufilfil	$⊢ L \in UFil (Y) \to L \in Fil (Y)$
2		filfbas	$⊢ L \in Fil (Y) \to L \in fBas (Y)$
3	1 2	syl	$⊢ L \in UFil (Y) \to L \in fBas (Y)$
4		fmfil	$⊢ (X \in A \land L \in fBas (Y) \land F : Y ⟶ X) \to (X FilMap F) (L) \in Fil (X)$
5	3 4	syl3an2	$⊢ (X \in A \land L \in UFil (Y) \land F : Y ⟶ X) \to (X FilMap F) (L) \in Fil (X)$
6		simpl2	$⊢ ((X \in A \land L \in UFil (Y) \land F : Y ⟶ X) \land (f \in Fil (X) \land (X FilMap F) (L) \subseteq f)) \to L \in UFil (Y)$
7	6 1 2	3syl	$⊢ ((X \in A \land L \in UFil (Y) \land F : Y ⟶ X) \land (f \in Fil (X) \land (X FilMap F) (L) \subseteq f)) \to L \in fBas (Y)$
8		simprl	$⊢ ((X \in A \land L \in UFil (Y) \land F : Y ⟶ X) \land (f \in Fil (X) \land (X FilMap F) (L) \subseteq f)) \to f \in Fil (X)$
9		simpl3	$⊢ ((X \in A \land L \in UFil (Y) \land F : Y ⟶ X) \land (f \in Fil (X) \land (X FilMap F) (L) \subseteq f)) \to F : Y ⟶ X$
10		simprr	$⊢ ((X \in A \land L \in UFil (Y) \land F : Y ⟶ X) \land (f \in Fil (X) \land (X FilMap F) (L) \subseteq f)) \to (X FilMap F) (L) \subseteq f$
11	7 8 9 10	fmfnfm	$⊢ ((X \in A \land L \in UFil (Y) \land F : Y ⟶ X) \land (f \in Fil (X) \land (X FilMap F) (L) \subseteq f)) \to \exists g \in Fil (Y) (L \subseteq g \land f = (X FilMap F) (g))$
12	6	adantr	$⊢ (((X \in A \land L \in UFil (Y) \land F : Y ⟶ X) \land (f \in Fil (X) \land (X FilMap F) (L) \subseteq f)) \land (g \in Fil (Y) \land (L \subseteq g \land f = (X FilMap F) (g)))) \to L \in UFil (Y)$
13		simprl	$⊢ (((X \in A \land L \in UFil (Y) \land F : Y ⟶ X) \land (f \in Fil (X) \land (X FilMap F) (L) \subseteq f)) \land (g \in Fil (Y) \land (L \subseteq g \land f = (X FilMap F) (g)))) \to g \in Fil (Y)$
14		simprrl	$⊢ (((X \in A \land L \in UFil (Y) \land F : Y ⟶ X) \land (f \in Fil (X) \land (X FilMap F) (L) \subseteq f)) \land (g \in Fil (Y) \land (L \subseteq g \land f = (X FilMap F) (g)))) \to L \subseteq g$
15		ufilmax	$⊢ (L \in UFil (Y) \land g \in Fil (Y) \land L \subseteq g) \to L = g$
16	12 13 14 15	syl3anc	$⊢ (((X \in A \land L \in UFil (Y) \land F : Y ⟶ X) \land (f \in Fil (X) \land (X FilMap F) (L) \subseteq f)) \land (g \in Fil (Y) \land (L \subseteq g \land f = (X FilMap F) (g)))) \to L = g$
17	16	fveq2d	$⊢ (((X \in A \land L \in UFil (Y) \land F : Y ⟶ X) \land (f \in Fil (X) \land (X FilMap F) (L) \subseteq f)) \land (g \in Fil (Y) \land (L \subseteq g \land f = (X FilMap F) (g)))) \to (X FilMap F) (L) = (X FilMap F) (g)$
18		simprrr	$⊢ (((X \in A \land L \in UFil (Y) \land F : Y ⟶ X) \land (f \in Fil (X) \land (X FilMap F) (L) \subseteq f)) \land (g \in Fil (Y) \land (L \subseteq g \land f = (X FilMap F) (g)))) \to f = (X FilMap F) (g)$
19	17 18	eqtr4d	$⊢ (((X \in A \land L \in UFil (Y) \land F : Y ⟶ X) \land (f \in Fil (X) \land (X FilMap F) (L) \subseteq f)) \land (g \in Fil (Y) \land (L \subseteq g \land f = (X FilMap F) (g)))) \to (X FilMap F) (L) = f$
20	11 19	rexlimddv	$⊢ ((X \in A \land L \in UFil (Y) \land F : Y ⟶ X) \land (f \in Fil (X) \land (X FilMap F) (L) \subseteq f)) \to (X FilMap F) (L) = f$
21	20	expr	$⊢ ((X \in A \land L \in UFil (Y) \land F : Y ⟶ X) \land f \in Fil (X)) \to ((X FilMap F) (L) \subseteq f \to (X FilMap F) (L) = f)$
22	21	ralrimiva	$⊢ (X \in A \land L \in UFil (Y) \land F : Y ⟶ X) \to \forall f \in Fil (X) ((X FilMap F) (L) \subseteq f \to (X FilMap F) (L) = f)$
23		isufil2	$⊢ (X FilMap F) (L) \in UFil (X) \leftrightarrow ((X FilMap F) (L) \in Fil (X) \land \forall f \in Fil (X) ((X FilMap F) (L) \subseteq f \to (X FilMap F) (L) = f))$
24	5 22 23	sylanbrc	$⊢ (X \in A \land L \in UFil (Y) \land F : Y ⟶ X) \to (X FilMap F) (L) \in UFil (X)$

Metamath Proof Explorer

Theorem fmufil

Proof