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

Metamath Proof Explorer

Theorem isfild

Proof