isfild

Description: Sufficient condition for a set of the form { x e. ~P A | ph } to be a filter. (Contributed by Mario Carneiro, 1-Dec-2013) (Revised by Stefan O'Rear, 2-Aug-2015) (Revised by AV, 10-Apr-2024)

	Ref	Expression
Hypotheses	isfild.1	$⊢ φ \to (x \in F \leftrightarrow (x \subseteq A \land ψ))$
	isfild.2	$⊢ φ \to A \in V$
	isfild.3	$⊢ φ \to \underset{˙}{[} A / x \underset{˙}{]} ψ$
	isfild.4	$⊢ φ \to \neg \underset{˙}{[} \emptyset / x \underset{˙}{]} ψ$
	isfild.5	$⊢ (φ \land y \subseteq A \land z \subseteq y) \to (\underset{˙}{[} z / x \underset{˙}{]} ψ \to \underset{˙}{[} y / x \underset{˙}{]} ψ)$
	isfild.6	$⊢ (φ \land y \subseteq A \land z \subseteq A) \to ((\underset{˙}{[} y / x \underset{˙}{]} ψ \land \underset{˙}{[} z / x \underset{˙}{]} ψ) \to \underset{˙}{[} (y \cap z) / x \underset{˙}{]} ψ)$
Assertion	isfild	$⊢ φ \to F \in Fil (A)$

Proof

Step	Hyp	Ref	Expression
1		isfild.1	$⊢ φ \to (x \in F \leftrightarrow (x \subseteq A \land ψ))$
2		isfild.2	$⊢ φ \to A \in V$
3		isfild.3	$⊢ φ \to \underset{˙}{[} A / x \underset{˙}{]} ψ$
4		isfild.4	$⊢ φ \to \neg \underset{˙}{[} \emptyset / x \underset{˙}{]} ψ$
5		isfild.5	$⊢ (φ \land y \subseteq A \land z \subseteq y) \to (\underset{˙}{[} z / x \underset{˙}{]} ψ \to \underset{˙}{[} y / x \underset{˙}{]} ψ)$
6		isfild.6	$⊢ (φ \land y \subseteq A \land z \subseteq A) \to ((\underset{˙}{[} y / x \underset{˙}{]} ψ \land \underset{˙}{[} z / x \underset{˙}{]} ψ) \to \underset{˙}{[} (y \cap z) / x \underset{˙}{]} ψ)$
7		velpw	$⊢ x \in 𝒫 A \leftrightarrow x \subseteq A$
8	7	biranri	$⊢ (x \subseteq A \land ψ) \to x \in 𝒫 A$
9	1 8	biimtrdi	$⊢ φ \to (x \in F \to x \in 𝒫 A)$
10	9	ssrdv	$⊢ φ \to F \subseteq 𝒫 A$
11	1 2	isfildlem	$⊢ φ \to (\emptyset \in F \leftrightarrow (\emptyset \subseteq A \land \underset{˙}{[} \emptyset / x \underset{˙}{]} ψ))$
12		simpr	$⊢ (\emptyset \subseteq A \land \underset{˙}{[} \emptyset / x \underset{˙}{]} ψ) \to \underset{˙}{[} \emptyset / x \underset{˙}{]} ψ$
13	11 12	biimtrdi	$⊢ φ \to (\emptyset \in F \to \underset{˙}{[} \emptyset / x \underset{˙}{]} ψ)$
14	4 13	mtod	$⊢ φ \to \neg \emptyset \in F$
15		ssid	$⊢ A \subseteq A$
16	3 15	jctil	$⊢ φ \to (A \subseteq A \land \underset{˙}{[} A / x \underset{˙}{]} ψ)$
17	1 2	isfildlem	$⊢ φ \to (A \in F \leftrightarrow (A \subseteq A \land \underset{˙}{[} A / x \underset{˙}{]} ψ))$
18	16 17	mpbird	$⊢ φ \to A \in F$
19	10 14 18	3jca	$⊢ φ \to (F \subseteq 𝒫 A \land \neg \emptyset \in F \land A \in F)$
20		elpwi	$⊢ y \in 𝒫 A \to y \subseteq A$
21		simp2	$⊢ (φ \land y \subseteq A \land z \subseteq y) \to y \subseteq A$
22	5 21	jctild	$⊢ (φ \land y \subseteq A \land z \subseteq y) \to (\underset{˙}{[} z / x \underset{˙}{]} ψ \to (y \subseteq A \land \underset{˙}{[} y / x \underset{˙}{]} ψ))$
23	22	adantld	$⊢ (φ \land y \subseteq A \land z \subseteq y) \to ((z \subseteq A \land \underset{˙}{[} z / x \underset{˙}{]} ψ) \to (y \subseteq A \land \underset{˙}{[} y / x \underset{˙}{]} ψ))$
24	1 2	isfildlem	$⊢ φ \to (z \in F \leftrightarrow (z \subseteq A \land \underset{˙}{[} z / x \underset{˙}{]} ψ))$
25	24	3ad2ant1	$⊢ (φ \land y \subseteq A \land z \subseteq y) \to (z \in F \leftrightarrow (z \subseteq A \land \underset{˙}{[} z / x \underset{˙}{]} ψ))$
26	1 2	isfildlem	$⊢ φ \to (y \in F \leftrightarrow (y \subseteq A \land \underset{˙}{[} y / x \underset{˙}{]} ψ))$
27	26	3ad2ant1	$⊢ (φ \land y \subseteq A \land z \subseteq y) \to (y \in F \leftrightarrow (y \subseteq A \land \underset{˙}{[} y / x \underset{˙}{]} ψ))$
28	23 25 27	3imtr4d	$⊢ (φ \land y \subseteq A \land z \subseteq y) \to (z \in F \to y \in F)$
29	28	3expa	$⊢ ((φ \land y \subseteq A) \land z \subseteq y) \to (z \in F \to y \in F)$
30	29	impancom	$⊢ ((φ \land y \subseteq A) \land z \in F) \to (z \subseteq y \to y \in F)$
31	30	rexlimdva	$⊢ (φ \land y \subseteq A) \to (\exists z \in F z \subseteq y \to y \in F)$
32	31	ex	$⊢ φ \to (y \subseteq A \to (\exists z \in F z \subseteq y \to y \in F))$
33	20 32	syl5	$⊢ φ \to (y \in 𝒫 A \to (\exists z \in F z \subseteq y \to y \in F))$
34	33	ralrimiv	$⊢ φ \to \forall y \in 𝒫 A (\exists z \in F z \subseteq y \to y \in F)$
35		ssinss1	$⊢ y \subseteq A \to y \cap z \subseteq A$
36	35	ad2antrr	$⊢ ((y \subseteq A \land \underset{˙}{[} y / x \underset{˙}{]} ψ) \land (z \subseteq A \land \underset{˙}{[} z / x \underset{˙}{]} ψ)) \to y \cap z \subseteq A$
37	36	a1i	$⊢ φ \to (((y \subseteq A \land \underset{˙}{[} y / x \underset{˙}{]} ψ) \land (z \subseteq A \land \underset{˙}{[} z / x \underset{˙}{]} ψ)) \to y \cap z \subseteq A)$
38		an4	$⊢ ((y \subseteq A \land \underset{˙}{[} y / x \underset{˙}{]} ψ) \land (z \subseteq A \land \underset{˙}{[} z / x \underset{˙}{]} ψ)) \leftrightarrow ((y \subseteq A \land z \subseteq A) \land (\underset{˙}{[} y / x \underset{˙}{]} ψ \land \underset{˙}{[} z / x \underset{˙}{]} ψ))$
39	6	3expb	$⊢ (φ \land (y \subseteq A \land z \subseteq A)) \to ((\underset{˙}{[} y / x \underset{˙}{]} ψ \land \underset{˙}{[} z / x \underset{˙}{]} ψ) \to \underset{˙}{[} (y \cap z) / x \underset{˙}{]} ψ)$
40	39	expimpd	$⊢ φ \to (((y \subseteq A \land z \subseteq A) \land (\underset{˙}{[} y / x \underset{˙}{]} ψ \land \underset{˙}{[} z / x \underset{˙}{]} ψ)) \to \underset{˙}{[} (y \cap z) / x \underset{˙}{]} ψ)$
41	38 40	biimtrid	$⊢ φ \to (((y \subseteq A \land \underset{˙}{[} y / x \underset{˙}{]} ψ) \land (z \subseteq A \land \underset{˙}{[} z / x \underset{˙}{]} ψ)) \to \underset{˙}{[} (y \cap z) / x \underset{˙}{]} ψ)$
42	37 41	jcad	$⊢ φ \to (((y \subseteq A \land \underset{˙}{[} y / x \underset{˙}{]} ψ) \land (z \subseteq A \land \underset{˙}{[} z / x \underset{˙}{]} ψ)) \to (y \cap z \subseteq A \land \underset{˙}{[} (y \cap z) / x \underset{˙}{]} ψ))$
43	26 24	anbi12d	$⊢ φ \to ((y \in F \land z \in F) \leftrightarrow ((y \subseteq A \land \underset{˙}{[} y / x \underset{˙}{]} ψ) \land (z \subseteq A \land \underset{˙}{[} z / x \underset{˙}{]} ψ)))$
44	1 2	isfildlem	$⊢ φ \to (y \cap z \in F \leftrightarrow (y \cap z \subseteq A \land \underset{˙}{[} (y \cap z) / x \underset{˙}{]} ψ))$
45	42 43 44	3imtr4d	$⊢ φ \to ((y \in F \land z \in F) \to y \cap z \in F)$
46	45	ralrimivv	$⊢ φ \to \forall y \in F \forall z \in F y \cap z \in F$
47		isfil2	$⊢ F \in Fil (A) \leftrightarrow ((F \subseteq 𝒫 A \land \neg \emptyset \in F \land A \in F) \land \forall y \in 𝒫 A (\exists z \in F z \subseteq y \to y \in F) \land \forall y \in F \forall z \in F y \cap z \in F)$
48	19 34 46 47	syl3anbrc	$⊢ φ \to F \in Fil (A)$

Metamath Proof Explorer

Theorem isfild

Proof