trufil

Description: Conditions for the trace of an ultrafilter L to be an ultrafilter. (Contributed by Mario Carneiro, 27-Aug-2015)

		Ref	Expression
	Assertion	trufil	$⊢ (L \in UFil (Y) \land A \subseteq Y) \to (L ↾_{𝑡} A \in UFil (A) \leftrightarrow A \in L)$

Proof

Step	Hyp	Ref	Expression
1		ufilfil	$⊢ L ↾_{𝑡} A \in UFil (A) \to L ↾_{𝑡} A \in Fil (A)$
2		ufilfil	$⊢ L \in UFil (Y) \to L \in Fil (Y)$
3		trfil3	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to (L ↾_{𝑡} A \in Fil (A) \leftrightarrow \neg Y ∖ A \in L)$
4	2 3	sylan	$⊢ (L \in UFil (Y) \land A \subseteq Y) \to (L ↾_{𝑡} A \in Fil (A) \leftrightarrow \neg Y ∖ A \in L)$
5	1 4	imbitrid	$⊢ (L \in UFil (Y) \land A \subseteq Y) \to (L ↾_{𝑡} A \in UFil (A) \to \neg Y ∖ A \in L)$
6	4	biimprd	$⊢ (L \in UFil (Y) \land A \subseteq Y) \to (\neg Y ∖ A \in L \to L ↾_{𝑡} A \in Fil (A))$
7		elpwi	$⊢ x \in 𝒫 A \to x \subseteq A$
8		simpll	$⊢ ((L \in UFil (Y) \land A \subseteq Y) \land x \subseteq A) \to L \in UFil (Y)$
9		simpr	$⊢ ((L \in UFil (Y) \land A \subseteq Y) \land x \subseteq A) \to x \subseteq A$
10		simplr	$⊢ ((L \in UFil (Y) \land A \subseteq Y) \land x \subseteq A) \to A \subseteq Y$
11	9 10	sstrd	$⊢ ((L \in UFil (Y) \land A \subseteq Y) \land x \subseteq A) \to x \subseteq Y$
12		ufilss	$⊢ (L \in UFil (Y) \land x \subseteq Y) \to (x \in L \lor Y ∖ x \in L)$
13	8 11 12	syl2anc	$⊢ ((L \in UFil (Y) \land A \subseteq Y) \land x \subseteq A) \to (x \in L \lor Y ∖ x \in L)$
14		id	$⊢ A \subseteq Y \to A \subseteq Y$
15		elfvdm	$⊢ L \in UFil (Y) \to Y \in dom UFil$
16		ssexg	$⊢ (A \subseteq Y \land Y \in dom UFil) \to A \in V$
17	14 15 16	syl2anr	$⊢ (L \in UFil (Y) \land A \subseteq Y) \to A \in V$
18		elrestr	$⊢ (L \in UFil (Y) \land A \in V \land x \in L) \to x \cap A \in (L ↾_{𝑡} A)$
19	18	3expia	$⊢ (L \in UFil (Y) \land A \in V) \to (x \in L \to x \cap A \in (L ↾_{𝑡} A))$
20	17 19	syldan	$⊢ (L \in UFil (Y) \land A \subseteq Y) \to (x \in L \to x \cap A \in (L ↾_{𝑡} A))$
21	20	adantr	$⊢ ((L \in UFil (Y) \land A \subseteq Y) \land x \subseteq A) \to (x \in L \to x \cap A \in (L ↾_{𝑡} A))$
22		df-ss	$⊢ x \subseteq A \leftrightarrow x \cap A = x$
23	9 22	sylib	$⊢ ((L \in UFil (Y) \land A \subseteq Y) \land x \subseteq A) \to x \cap A = x$
24	23	eleq1d	$⊢ ((L \in UFil (Y) \land A \subseteq Y) \land x \subseteq A) \to (x \cap A \in (L ↾_{𝑡} A) \leftrightarrow x \in (L ↾_{𝑡} A))$
25	21 24	sylibd	$⊢ ((L \in UFil (Y) \land A \subseteq Y) \land x \subseteq A) \to (x \in L \to x \in (L ↾_{𝑡} A))$
26		indif1	$⊢ (Y ∖ x) \cap A = (Y \cap A) ∖ x$
27		simplr	$⊢ ((L \in UFil (Y) \land A \subseteq Y) \land (x \subseteq A \land Y ∖ x \in L)) \to A \subseteq Y$
28		sseqin2	$⊢ A \subseteq Y \leftrightarrow Y \cap A = A$
29	27 28	sylib	$⊢ ((L \in UFil (Y) \land A \subseteq Y) \land (x \subseteq A \land Y ∖ x \in L)) \to Y \cap A = A$
30	29	difeq1d	$⊢ ((L \in UFil (Y) \land A \subseteq Y) \land (x \subseteq A \land Y ∖ x \in L)) \to (Y \cap A) ∖ x = A ∖ x$
31	26 30	eqtrid	$⊢ ((L \in UFil (Y) \land A \subseteq Y) \land (x \subseteq A \land Y ∖ x \in L)) \to (Y ∖ x) \cap A = A ∖ x$
32		simpll	$⊢ ((L \in UFil (Y) \land A \subseteq Y) \land (x \subseteq A \land Y ∖ x \in L)) \to L \in UFil (Y)$
33	17	adantr	$⊢ ((L \in UFil (Y) \land A \subseteq Y) \land (x \subseteq A \land Y ∖ x \in L)) \to A \in V$
34		simprr	$⊢ ((L \in UFil (Y) \land A \subseteq Y) \land (x \subseteq A \land Y ∖ x \in L)) \to Y ∖ x \in L$
35		elrestr	$⊢ (L \in UFil (Y) \land A \in V \land Y ∖ x \in L) \to (Y ∖ x) \cap A \in (L ↾_{𝑡} A)$
36	32 33 34 35	syl3anc	$⊢ ((L \in UFil (Y) \land A \subseteq Y) \land (x \subseteq A \land Y ∖ x \in L)) \to (Y ∖ x) \cap A \in (L ↾_{𝑡} A)$
37	31 36	eqeltrrd	$⊢ ((L \in UFil (Y) \land A \subseteq Y) \land (x \subseteq A \land Y ∖ x \in L)) \to A ∖ x \in (L ↾_{𝑡} A)$
38	37	expr	$⊢ ((L \in UFil (Y) \land A \subseteq Y) \land x \subseteq A) \to (Y ∖ x \in L \to A ∖ x \in (L ↾_{𝑡} A))$
39	25 38	orim12d	$⊢ ((L \in UFil (Y) \land A \subseteq Y) \land x \subseteq A) \to ((x \in L \lor Y ∖ x \in L) \to (x \in (L ↾_{𝑡} A) \lor A ∖ x \in (L ↾_{𝑡} A)))$
40	13 39	mpd	$⊢ ((L \in UFil (Y) \land A \subseteq Y) \land x \subseteq A) \to (x \in (L ↾_{𝑡} A) \lor A ∖ x \in (L ↾_{𝑡} A))$
41	7 40	sylan2	$⊢ ((L \in UFil (Y) \land A \subseteq Y) \land x \in 𝒫 A) \to (x \in (L ↾_{𝑡} A) \lor A ∖ x \in (L ↾_{𝑡} A))$
42	41	ralrimiva	$⊢ (L \in UFil (Y) \land A \subseteq Y) \to \forall x \in 𝒫 A (x \in (L ↾_{𝑡} A) \lor A ∖ x \in (L ↾_{𝑡} A))$
43	6 42	jctird	$⊢ (L \in UFil (Y) \land A \subseteq Y) \to (\neg Y ∖ A \in L \to (L ↾_{𝑡} A \in Fil (A) \land \forall x \in 𝒫 A (x \in (L ↾_{𝑡} A) \lor A ∖ x \in (L ↾_{𝑡} A))))$
44		isufil	$⊢ L ↾_{𝑡} A \in UFil (A) \leftrightarrow (L ↾_{𝑡} A \in Fil (A) \land \forall x \in 𝒫 A (x \in (L ↾_{𝑡} A) \lor A ∖ x \in (L ↾_{𝑡} A)))$
45	43 44	imbitrrdi	$⊢ (L \in UFil (Y) \land A \subseteq Y) \to (\neg Y ∖ A \in L \to L ↾_{𝑡} A \in UFil (A))$
46	5 45	impbid	$⊢ (L \in UFil (Y) \land A \subseteq Y) \to (L ↾_{𝑡} A \in UFil (A) \leftrightarrow \neg Y ∖ A \in L)$
47		ufilb	$⊢ (L \in UFil (Y) \land A \subseteq Y) \to (\neg A \in L \leftrightarrow Y ∖ A \in L)$
48	47	con1bid	$⊢ (L \in UFil (Y) \land A \subseteq Y) \to (\neg Y ∖ A \in L \leftrightarrow A \in L)$
49	46 48	bitrd	$⊢ (L \in UFil (Y) \land A \subseteq Y) \to (L ↾_{𝑡} A \in UFil (A) \leftrightarrow A \in L)$

Metamath Proof Explorer

Theorem trufil

Proof