ssufl

Description: If Y is a subset of X and filters extend to ultrafilters in X , then they still do in Y . (Contributed by Mario Carneiro, 26-Aug-2015)

		Ref	Expression
	Assertion	ssufl	$⊢ (X \in UFL \land Y \subseteq X) \to Y \in UFL$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \to X \in UFL$
2		filfbas	$⊢ f \in Fil (Y) \to f \in fBas (Y)$
3	2	adantl	$⊢ ((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \to f \in fBas (Y)$
4		filsspw	$⊢ f \in Fil (Y) \to f \subseteq 𝒫 Y$
5	4	adantl	$⊢ ((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \to f \subseteq 𝒫 Y$
6		simplr	$⊢ ((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \to Y \subseteq X$
7	6	sspwd	$⊢ ((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \to 𝒫 Y \subseteq 𝒫 X$
8	5 7	sstrd	$⊢ ((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \to f \subseteq 𝒫 X$
9		fbasweak	$⊢ (f \in fBas (Y) \land f \subseteq 𝒫 X \land X \in UFL) \to f \in fBas (X)$
10	3 8 1 9	syl3anc	$⊢ ((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \to f \in fBas (X)$
11		fgcl	$⊢ f \in fBas (X) \to X filGen f \in Fil (X)$
12	10 11	syl	$⊢ ((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \to X filGen f \in Fil (X)$
13		ufli	$⊢ (X \in UFL \land X filGen f \in Fil (X)) \to \exists u \in UFil (X) X filGen f \subseteq u$
14	1 12 13	syl2anc	$⊢ ((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \to \exists u \in UFil (X) X filGen f \subseteq u$
15		ssfg	$⊢ f \in fBas (X) \to f \subseteq X filGen f$
16	10 15	syl	$⊢ ((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \to f \subseteq X filGen f$
17	16	adantr	$⊢ (((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \land (u \in UFil (X) \land X filGen f \subseteq u)) \to f \subseteq X filGen f$
18		simprr	$⊢ (((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \land (u \in UFil (X) \land X filGen f \subseteq u)) \to X filGen f \subseteq u$
19	17 18	sstrd	$⊢ (((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \land (u \in UFil (X) \land X filGen f \subseteq u)) \to f \subseteq u$
20		filtop	$⊢ f \in Fil (Y) \to Y \in f$
21	20	ad2antlr	$⊢ (((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \land (u \in UFil (X) \land X filGen f \subseteq u)) \to Y \in f$
22	19 21	sseldd	$⊢ (((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \land (u \in UFil (X) \land X filGen f \subseteq u)) \to Y \in u$
23		simprl	$⊢ (((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \land (u \in UFil (X) \land X filGen f \subseteq u)) \to u \in UFil (X)$
24	6	adantr	$⊢ (((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \land (u \in UFil (X) \land X filGen f \subseteq u)) \to Y \subseteq X$
25		trufil	$⊢ (u \in UFil (X) \land Y \subseteq X) \to (u ↾_{𝑡} Y \in UFil (Y) \leftrightarrow Y \in u)$
26	23 24 25	syl2anc	$⊢ (((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \land (u \in UFil (X) \land X filGen f \subseteq u)) \to (u ↾_{𝑡} Y \in UFil (Y) \leftrightarrow Y \in u)$
27	22 26	mpbird	$⊢ (((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \land (u \in UFil (X) \land X filGen f \subseteq u)) \to u ↾_{𝑡} Y \in UFil (Y)$
28	5	adantr	$⊢ (((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \land (u \in UFil (X) \land X filGen f \subseteq u)) \to f \subseteq 𝒫 Y$
29		restid2	$⊢ (Y \in f \land f \subseteq 𝒫 Y) \to f ↾_{𝑡} Y = f$
30	21 28 29	syl2anc	$⊢ (((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \land (u \in UFil (X) \land X filGen f \subseteq u)) \to f ↾_{𝑡} Y = f$
31		ssrest	$⊢ (u \in UFil (X) \land f \subseteq u) \to f ↾_{𝑡} Y \subseteq u ↾_{𝑡} Y$
32	23 19 31	syl2anc	$⊢ (((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \land (u \in UFil (X) \land X filGen f \subseteq u)) \to f ↾_{𝑡} Y \subseteq u ↾_{𝑡} Y$
33	30 32	eqsstrrd	$⊢ (((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \land (u \in UFil (X) \land X filGen f \subseteq u)) \to f \subseteq u ↾_{𝑡} Y$
34		sseq2	$⊢ g = u ↾_{𝑡} Y \to (f \subseteq g \leftrightarrow f \subseteq u ↾_{𝑡} Y)$
35	34	rspcev	$⊢ (u ↾_{𝑡} Y \in UFil (Y) \land f \subseteq u ↾_{𝑡} Y) \to \exists g \in UFil (Y) f \subseteq g$
36	27 33 35	syl2anc	$⊢ (((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \land (u \in UFil (X) \land X filGen f \subseteq u)) \to \exists g \in UFil (Y) f \subseteq g$
37	14 36	rexlimddv	$⊢ ((X \in UFL \land Y \subseteq X) \land f \in Fil (Y)) \to \exists g \in UFil (Y) f \subseteq g$
38	37	ralrimiva	$⊢ (X \in UFL \land Y \subseteq X) \to \forall f \in Fil (Y) \exists g \in UFil (Y) f \subseteq g$
39		ssexg	$⊢ (Y \subseteq X \land X \in UFL) \to Y \in V$
40	39	ancoms	$⊢ (X \in UFL \land Y \subseteq X) \to Y \in V$
41		isufl	$⊢ Y \in V \to (Y \in UFL \leftrightarrow \forall f \in Fil (Y) \exists g \in UFil (Y) f \subseteq g)$
42	40 41	syl	$⊢ (X \in UFL \land Y \subseteq X) \to (Y \in UFL \leftrightarrow \forall f \in Fil (Y) \exists g \in UFil (Y) f \subseteq g)$
43	38 42	mpbird	$⊢ (X \in UFL \land Y \subseteq X) \to Y \in UFL$

Metamath Proof Explorer

Theorem ssufl

Proof