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	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐹 ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝜓 ) ) )
	isfild.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	isfild.3	⊢ ( 𝜑 → [ 𝐴 / 𝑥 ] 𝜓 )
	isfild.4	⊢ ( 𝜑 → ¬ [ ∅ / 𝑥 ] 𝜓 )
	isfild.5	⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝑦 ) → ( [ 𝑧 / 𝑥 ] 𝜓 → [ 𝑦 / 𝑥 ] 𝜓 ) )
	isfild.6	⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐴 ) → ( ( [ 𝑦 / 𝑥 ] 𝜓 ∧ [ 𝑧 / 𝑥 ] 𝜓 ) → [ ( 𝑦 ∩ 𝑧 ) / 𝑥 ] 𝜓 ) )
Assertion	isfild	⊢ ( 𝜑 → 𝐹 ∈ ( Fil ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		isfild.1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐹 ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝜓 ) ) )
2		isfild.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		isfild.3	⊢ ( 𝜑 → [ 𝐴 / 𝑥 ] 𝜓 )
4		isfild.4	⊢ ( 𝜑 → ¬ [ ∅ / 𝑥 ] 𝜓 )
5		isfild.5	⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝑦 ) → ( [ 𝑧 / 𝑥 ] 𝜓 → [ 𝑦 / 𝑥 ] 𝜓 ) )
6		isfild.6	⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐴 ) → ( ( [ 𝑦 / 𝑥 ] 𝜓 ∧ [ 𝑧 / 𝑥 ] 𝜓 ) → [ ( 𝑦 ∩ 𝑧 ) / 𝑥 ] 𝜓 ) )
7		velpw	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
8	7	biranri	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝜓 ) → 𝑥 ∈ 𝒫 𝐴 )
9	1 8	biimtrdi	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐹 → 𝑥 ∈ 𝒫 𝐴 ) )
10	9	ssrdv	⊢ ( 𝜑 → 𝐹 ⊆ 𝒫 𝐴 )
11	1 2	isfildlem	⊢ ( 𝜑 → ( ∅ ∈ 𝐹 ↔ ( ∅ ⊆ 𝐴 ∧ [ ∅ / 𝑥 ] 𝜓 ) ) )
12		simpr	⊢ ( ( ∅ ⊆ 𝐴 ∧ [ ∅ / 𝑥 ] 𝜓 ) → [ ∅ / 𝑥 ] 𝜓 )
13	11 12	biimtrdi	⊢ ( 𝜑 → ( ∅ ∈ 𝐹 → [ ∅ / 𝑥 ] 𝜓 ) )
14	4 13	mtod	⊢ ( 𝜑 → ¬ ∅ ∈ 𝐹 )
15		ssid	⊢ 𝐴 ⊆ 𝐴
16	3 15	jctil	⊢ ( 𝜑 → ( 𝐴 ⊆ 𝐴 ∧ [ 𝐴 / 𝑥 ] 𝜓 ) )
17	1 2	isfildlem	⊢ ( 𝜑 → ( 𝐴 ∈ 𝐹 ↔ ( 𝐴 ⊆ 𝐴 ∧ [ 𝐴 / 𝑥 ] 𝜓 ) ) )
18	16 17	mpbird	⊢ ( 𝜑 → 𝐴 ∈ 𝐹 )
19	10 14 18	3jca	⊢ ( 𝜑 → ( 𝐹 ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝐴 ∈ 𝐹 ) )
20		elpwi	⊢ ( 𝑦 ∈ 𝒫 𝐴 → 𝑦 ⊆ 𝐴 )
21		simp2	⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝑦 ) → 𝑦 ⊆ 𝐴 )
22	5 21	jctild	⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝑦 ) → ( [ 𝑧 / 𝑥 ] 𝜓 → ( 𝑦 ⊆ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ) )
23	22	adantld	⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝑦 ) → ( ( 𝑧 ⊆ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜓 ) → ( 𝑦 ⊆ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ) )
24	1 2	isfildlem	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐹 ↔ ( 𝑧 ⊆ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜓 ) ) )
25	24	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝑦 ) → ( 𝑧 ∈ 𝐹 ↔ ( 𝑧 ⊆ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜓 ) ) )
26	1 2	isfildlem	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐹 ↔ ( 𝑦 ⊆ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ) )
27	26	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝑦 ) → ( 𝑦 ∈ 𝐹 ↔ ( 𝑦 ⊆ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ) )
28	23 25 27	3imtr4d	⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝑦 ) → ( 𝑧 ∈ 𝐹 → 𝑦 ∈ 𝐹 ) )
29	28	3expa	⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑧 ⊆ 𝑦 ) → ( 𝑧 ∈ 𝐹 → 𝑦 ∈ 𝐹 ) )
30	29	impancom	⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑧 ∈ 𝐹 ) → ( 𝑧 ⊆ 𝑦 → 𝑦 ∈ 𝐹 ) )
31	30	rexlimdva	⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ) → ( ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦 → 𝑦 ∈ 𝐹 ) )
32	31	ex	⊢ ( 𝜑 → ( 𝑦 ⊆ 𝐴 → ( ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦 → 𝑦 ∈ 𝐹 ) ) )
33	20 32	syl5	⊢ ( 𝜑 → ( 𝑦 ∈ 𝒫 𝐴 → ( ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦 → 𝑦 ∈ 𝐹 ) ) )
34	33	ralrimiv	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝒫 𝐴 ( ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦 → 𝑦 ∈ 𝐹 ) )
35		ssinss1	⊢ ( 𝑦 ⊆ 𝐴 → ( 𝑦 ∩ 𝑧 ) ⊆ 𝐴 )
36	35	ad2antrr	⊢ ( ( ( 𝑦 ⊆ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ∧ ( 𝑧 ⊆ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜓 ) ) → ( 𝑦 ∩ 𝑧 ) ⊆ 𝐴 )
37	36	a1i	⊢ ( 𝜑 → ( ( ( 𝑦 ⊆ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ∧ ( 𝑧 ⊆ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜓 ) ) → ( 𝑦 ∩ 𝑧 ) ⊆ 𝐴 ) )
38		an4	⊢ ( ( ( 𝑦 ⊆ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ∧ ( 𝑧 ⊆ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜓 ) ) ↔ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐴 ) ∧ ( [ 𝑦 / 𝑥 ] 𝜓 ∧ [ 𝑧 / 𝑥 ] 𝜓 ) ) )
39	6	3expb	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐴 ) ) → ( ( [ 𝑦 / 𝑥 ] 𝜓 ∧ [ 𝑧 / 𝑥 ] 𝜓 ) → [ ( 𝑦 ∩ 𝑧 ) / 𝑥 ] 𝜓 ) )
40	39	expimpd	⊢ ( 𝜑 → ( ( ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐴 ) ∧ ( [ 𝑦 / 𝑥 ] 𝜓 ∧ [ 𝑧 / 𝑥 ] 𝜓 ) ) → [ ( 𝑦 ∩ 𝑧 ) / 𝑥 ] 𝜓 ) )
41	38 40	biimtrid	⊢ ( 𝜑 → ( ( ( 𝑦 ⊆ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ∧ ( 𝑧 ⊆ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜓 ) ) → [ ( 𝑦 ∩ 𝑧 ) / 𝑥 ] 𝜓 ) )
42	37 41	jcad	⊢ ( 𝜑 → ( ( ( 𝑦 ⊆ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ∧ ( 𝑧 ⊆ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜓 ) ) → ( ( 𝑦 ∩ 𝑧 ) ⊆ 𝐴 ∧ [ ( 𝑦 ∩ 𝑧 ) / 𝑥 ] 𝜓 ) ) )
43	26 24	anbi12d	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) ↔ ( ( 𝑦 ⊆ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ∧ ( 𝑧 ⊆ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜓 ) ) ) )
44	1 2	isfildlem	⊢ ( 𝜑 → ( ( 𝑦 ∩ 𝑧 ) ∈ 𝐹 ↔ ( ( 𝑦 ∩ 𝑧 ) ⊆ 𝐴 ∧ [ ( 𝑦 ∩ 𝑧 ) / 𝑥 ] 𝜓 ) ) )
45	42 43 44	3imtr4d	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) → ( 𝑦 ∩ 𝑧 ) ∈ 𝐹 ) )
46	45	ralrimivv	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐹 ∀ 𝑧 ∈ 𝐹 ( 𝑦 ∩ 𝑧 ) ∈ 𝐹 )
47		isfil2	⊢ ( 𝐹 ∈ ( Fil ‘ 𝐴 ) ↔ ( ( 𝐹 ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝐴 ∈ 𝐹 ) ∧ ∀ 𝑦 ∈ 𝒫 𝐴 ( ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦 → 𝑦 ∈ 𝐹 ) ∧ ∀ 𝑦 ∈ 𝐹 ∀ 𝑧 ∈ 𝐹 ( 𝑦 ∩ 𝑧 ) ∈ 𝐹 ) )
48	19 34 46 47	syl3anbrc	⊢ ( 𝜑 → 𝐹 ∈ ( Fil ‘ 𝐴 ) )

Metamath Proof Explorer

Theorem isfild

Proof