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	biimpri	$⊢ x \subseteq A \to x \in 𝒫 A$
9	8	adantr	$⊢ (x \subseteq A \land ψ) \to x \in 𝒫 A$
10	1 9	syl6bi	$⊢ φ \to (x \in F \to x \in 𝒫 A)$
11	10	ssrdv	$⊢ φ \to F \subseteq 𝒫 A$
12	1 2	isfildlem	$⊢ φ \to (\emptyset \in F \leftrightarrow (\emptyset \subseteq A \land \underset{˙}{[} \emptyset / x \underset{˙}{]} ψ))$
13		simpr	$⊢ (\emptyset \subseteq A \land \underset{˙}{[} \emptyset / x \underset{˙}{]} ψ) \to \underset{˙}{[} \emptyset / x \underset{˙}{]} ψ$
14	12 13	syl6bi	$⊢ φ \to (\emptyset \in F \to \underset{˙}{[} \emptyset / x \underset{˙}{]} ψ)$
15	4 14	mtod	$⊢ φ \to \neg \emptyset \in F$
16		ssid	$⊢ A \subseteq A$
17	3 16	jctil	$⊢ φ \to (A \subseteq A \land \underset{˙}{[} A / x \underset{˙}{]} ψ)$
18	1 2	isfildlem	$⊢ φ \to (A \in F \leftrightarrow (A \subseteq A \land \underset{˙}{[} A / x \underset{˙}{]} ψ))$
19	17 18	mpbird	$⊢ φ \to A \in F$
20	11 15 19	3jca	$⊢ φ \to (F \subseteq 𝒫 A \land \neg \emptyset \in F \land A \in F)$
21		elpwi	$⊢ y \in 𝒫 A \to y \subseteq A$
22		simp2	$⊢ (φ \land y \subseteq A \land z \subseteq y) \to y \subseteq A$
23	5 22	jctild	$⊢ (φ \land y \subseteq A \land z \subseteq y) \to (\underset{˙}{[} z / x \underset{˙}{]} ψ \to (y \subseteq A \land \underset{˙}{[} y / x \underset{˙}{]} ψ))$
24	23	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{˙}{]} ψ))$
25	1 2	isfildlem	$⊢ φ \to (z \in F \leftrightarrow (z \subseteq A \land \underset{˙}{[} z / x \underset{˙}{]} ψ))$
26	25	3ad2ant1	$⊢ (φ \land y \subseteq A \land z \subseteq y) \to (z \in F \leftrightarrow (z \subseteq A \land \underset{˙}{[} z / x \underset{˙}{]} ψ))$
27	1 2	isfildlem	$⊢ φ \to (y \in F \leftrightarrow (y \subseteq A \land \underset{˙}{[} y / x \underset{˙}{]} ψ))$
28	27	3ad2ant1	$⊢ (φ \land y \subseteq A \land z \subseteq y) \to (y \in F \leftrightarrow (y \subseteq A \land \underset{˙}{[} y / x \underset{˙}{]} ψ))$
29	24 26 28	3imtr4d	$⊢ (φ \land y \subseteq A \land z \subseteq y) \to (z \in F \to y \in F)$
30	29	3expa	$⊢ ((φ \land y \subseteq A) \land z \subseteq y) \to (z \in F \to y \in F)$
31	30	impancom	$⊢ ((φ \land y \subseteq A) \land z \in F) \to (z \subseteq y \to y \in F)$
32	31	rexlimdva	$⊢ (φ \land y \subseteq A) \to (\exists z \in F z \subseteq y \to y \in F)$
33	32	ex	$⊢ φ \to (y \subseteq A \to (\exists z \in F z \subseteq y \to y \in F))$
34	21 33	syl5	$⊢ φ \to (y \in 𝒫 A \to (\exists z \in F z \subseteq y \to y \in F))$
35	34	ralrimiv	$⊢ φ \to \forall y \in 𝒫 A (\exists z \in F z \subseteq y \to y \in F)$
36		ssinss1	$⊢ y \subseteq A \to y \cap z \subseteq A$
37	36	ad2antrr	$⊢ ((y \subseteq A \land \underset{˙}{[} y / x \underset{˙}{]} ψ) \land (z \subseteq A \land \underset{˙}{[} z / x \underset{˙}{]} ψ)) \to y \cap z \subseteq A$
38	37	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)$
39		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{˙}{]} ψ))$
40	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{˙}{]} ψ)$
41	40	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{˙}{]} ψ)$
42	39 41	syl5bi	$⊢ φ \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{˙}{]} ψ)$
43	38 42	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{˙}{]} ψ))$
44	27 25	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{˙}{]} ψ)))$
45	1 2	isfildlem	$⊢ φ \to (y \cap z \in F \leftrightarrow (y \cap z \subseteq A \land \underset{˙}{[} (y \cap z) / x \underset{˙}{]} ψ))$
46	43 44 45	3imtr4d	$⊢ φ \to ((y \in F \land z \in F) \to y \cap z \in F)$
47	46	ralrimivv	$⊢ φ \to \forall y \in F \forall z \in F y \cap z \in F$
48		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)$
49	20 35 47 48	syl3anbrc	$⊢ φ \to F \in Fil (A)$

Metamath Proof Explorer

Theorem isfild

Proof