Theorem fillsb 10546

Description: A filter is closed under taking supersets.

Hypothesis

Ref	Expression
fillsb.1	⊢ X = ∪F

Assertion

Ref	Expression
fillsb	⊢ (F ∈ Fil → ((A ∈ F ⋀ B ⊆ X ⋀ A ⊆ B) → B ∈ F))

Proof of Theorem fillsb

Step	Hyp	Ref	Expression
1		uniexg 2877	. . . 4 ⊢ (F ∈ Fil → ∪F ∈ V)
2		fillsb.1	. . . 4 ⊢ X = ∪F
3	1, 2	syl5eqel 1555	. . 3 ⊢ (F ∈ Fil → X ∈ V)
4		elpw2g 2732	. . . . . . . 8 ⊢ (X ∈ V → (B ∈ ℘X ↔ B ⊆ X))
5	4	bicomd 523	. . . . . . 7 ⊢ (X ∈ V → (B ⊆ X ↔ B ∈ ℘X))
6	5	anbi2d 618	. . . . . 6 ⊢ (X ∈ V → ((A ∈ F ⋀ B ⊆ X) ↔ (A ∈ F ⋀ B ∈ ℘X)))
7		3simpa 787	. . . . . 6 ⊢ ((A ∈ F ⋀ B ⊆ X ⋀ A ⊆ B) → (A ∈ F ⋀ B ⊆ X))
8	6, 7	syl5bi 208	. . . . 5 ⊢ (X ∈ V → ((A ∈ F ⋀ B ⊆ X ⋀ A ⊆ B) → (A ∈ F ⋀ B ∈ ℘X)))
9		eleq1 1537	. . . . . . . . 9 ⊢ (x = A → (x ∈ F ↔ A ∈ F))
10		sseq1 2085	. . . . . . . . 9 ⊢ (x = A → (x ⊆ y ↔ A ⊆ y))
11	9, 10	3anbi13d 897	. . . . . . . 8 ⊢ (x = A → ((x ∈ F ⋀ y ⊆ X ⋀ x ⊆ y) ↔ (A ∈ F ⋀ y ⊆ X ⋀ A ⊆ y)))
12	11	imbi1d 615	. . . . . . 7 ⊢ (x = A → (((x ∈ F ⋀ y ⊆ X ⋀ x ⊆ y) → y ∈ F) ↔ ((A ∈ F ⋀ y ⊆ X ⋀ A ⊆ y) → y ∈ F)))
13	12	imbi2d 614	. . . . . 6 ⊢ (x = A → ((F ∈ Fil → ((x ∈ F ⋀ y ⊆ X ⋀ x ⊆ y) → y ∈ F)) ↔ (F ∈ Fil → ((A ∈ F ⋀ y ⊆ X ⋀ A ⊆ y) → y ∈ F))))
14		sseq1 2085	. . . . . . . . 9 ⊢ (y = B → (y ⊆ X ↔ B ⊆ X))
15		sseq2 2086	. . . . . . . . 9 ⊢ (y = B → (A ⊆ y ↔ A ⊆ B))
16	14, 15	3anbi23d 898	. . . . . . . 8 ⊢ (y = B → ((A ∈ F ⋀ y ⊆ X ⋀ A ⊆ y) ↔ (A ∈ F ⋀ B ⊆ X ⋀ A ⊆ B)))
17		eleq1 1537	. . . . . . . 8 ⊢ (y = B → (y ∈ F ↔ B ∈ F))
18	16, 17	imbi12d 628	. . . . . . 7 ⊢ (y = B → (((A ∈ F ⋀ y ⊆ X ⋀ A ⊆ y) → y ∈ F) ↔ ((A ∈ F ⋀ B ⊆ X ⋀ A ⊆ B) → B ∈ F)))
19	18	imbi2d 614	. . . . . 6 ⊢ (y = B → ((F ∈ Fil → ((A ∈ F ⋀ y ⊆ X ⋀ A ⊆ y) → y ∈ F)) ↔ (F ∈ Fil → ((A ∈ F ⋀ B ⊆ X ⋀ A ⊆ B) → B ∈ F))))
20	2	isfil 10544	. . . . . . . . 9 ⊢ (F ∈ Fil → (F ∈ Fil ↔ ((¬ ∅ ∈ F ⋀ X ∈ F) ⋀ ∀x∀y((x ∈ F ⋀ y ⊆ X ⋀ x ⊆ y) → y ∈ F) ⋀ ∀x ∈ F ∀y ∈ F (x ∩ y) ∈ F)))
21	20	ibi 594	. . . . . . . 8 ⊢ (F ∈ Fil → ((¬ ∅ ∈ F ⋀ X ∈ F) ⋀ ∀x∀y((x ∈ F ⋀ y ⊆ X ⋀ x ⊆ y) → y ∈ F) ⋀ ∀x ∈ F ∀y ∈ F (x ∩ y) ∈ F))
22	21	3simp2d 797	. . . . . . 7 ⊢ (F ∈ Fil → ∀x∀y((x ∈ F ⋀ y ⊆ X ⋀ x ⊆ y) → y ∈ F))
23	22	19.21bbi 1063	. . . . . 6 ⊢ (F ∈ Fil → ((x ∈ F ⋀ y ⊆ X ⋀ x ⊆ y) → y ∈ F))
24	13, 19, 23	vtocl2g 1853	. . . . 5 ⊢ ((A ∈ F ⋀ B ∈ ℘X) → (F ∈ Fil → ((A ∈ F ⋀ B ⊆ X ⋀ A ⊆ B) → B ∈ F)))
25	8, 24	syl6 22	. . . 4 ⊢ (X ∈ V → ((A ∈ F ⋀ B ⊆ X ⋀ A ⊆ B) → (F ∈ Fil → ((A ∈ F ⋀ B ⊆ X ⋀ A ⊆ B) → B ∈ F))))
26	25	com23 32	. . 3 ⊢ (X ∈ V → (F ∈ Fil → ((A ∈ F ⋀ B ⊆ X ⋀ A ⊆ B) → ((A ∈ F ⋀ B ⊆ X ⋀ A ⊆ B) → B ∈ F))))
27	3, 26	mpcom 49	. 2 ⊢ (F ∈ Fil → ((A ∈ F ⋀ B ⊆ X ⋀ A ⊆ B) → ((A ∈ F ⋀ B ⊆ X ⋀ A ⊆ B) → B ∈ F)))
28	27	pm2.43d 65	1 ⊢ (F ∈ Fil → ((A ∈ F ⋀ B ⊆ X ⋀ A ⊆ B) → B ∈ F))

Syntax hints:  ¬ wn 2   → wi 3   ⋀ wa 223   ⋀ w3a 777  ∀wal 956   = wceq 958   ∈ wcel 960  ∀wral 1648  Vcvv 1814   ∩ cin 2049   ⊆ wss 2050  ∅c0 2283  ℘cpw 2405  ∪cuni 2507  Filcfil 10542

This theorem is referenced by:  filintf 10554

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2708  ax-un 2872

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 779  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-ral 1652  df-v 1815  df-in 2054  df-ss 2056  df-pw 2406  df-uni 2508  df-fil 10543

Copyright terms: Public domain