fgabs - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fgabs		Structured version Visualization version GIF version

Theorem fgabs 23997

Description: Absorption law for filter generation. (Contributed by Mario Carneiro, 15-Oct-2015.)

**Assertion**
Ref	Expression
fgabs	⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹))

Proof of Theorem fgabs Dummy variables 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpll 778	. . . . . . . . 9 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑌))
2		fgcl 23996	. . . . . . . . 9 ⊢ (𝐹 ∈ (fBas‘𝑌) → (𝑌filGen𝐹) ∈ (Fil‘𝑌))
3		filfbas 23966	. . . . . . . . 9 ⊢ ((𝑌filGen𝐹) ∈ (Fil‘𝑌) → (𝑌filGen𝐹) ∈ (fBas‘𝑌))
4	1, 2, 3	3syl 19	. . . . . . . 8 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ∈ (fBas‘𝑌))
5		fbsspw 23950	. . . . . . . . . 10 ⊢ ((𝑌filGen𝐹) ∈ (fBas‘𝑌) → (𝑌filGen𝐹) ⊆ 𝒫 𝑌)
6	4, 5	syl 18	. . . . . . . . 9 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ⊆ 𝒫 𝑌)
7		simplr 780	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝑌 ⊆ 𝑋)
8	7	sspwd 4571	. . . . . . . . 9 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝒫 𝑌 ⊆ 𝒫 𝑋)
9	6, 8	sstrd 3949	. . . . . . . 8 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ⊆ 𝒫 𝑋)
10		simpr 489	. . . . . . . 8 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝑋 ∈ V)
11		fbasweak 23983	. . . . . . . 8 ⊢ (((𝑌filGen𝐹) ∈ (fBas‘𝑌) ∧ (𝑌filGen𝐹) ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ∈ (fBas‘𝑋))
12	4, 9, 10, 11	syl3anc 1394	. . . . . . 7 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ∈ (fBas‘𝑋))
13		elfg 23989	. . . . . . 7 ⊢ ((𝑌filGen𝐹) ∈ (fBas‘𝑋) → (𝑥 ∈ (𝑋filGen(𝑌filGen𝐹)) ↔ (𝑥 ⊆ 𝑋 ∧ ∃𝑦 ∈ (𝑌filGen𝐹)𝑦 ⊆ 𝑥)))
14	12, 13	syl 18	. . . . . 6 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑥 ∈ (𝑋filGen(𝑌filGen𝐹)) ↔ (𝑥 ⊆ 𝑋 ∧ ∃𝑦 ∈ (𝑌filGen𝐹)𝑦 ⊆ 𝑥)))
15	1	adantr 485	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ 𝑥 ⊆ 𝑋) → 𝐹 ∈ (fBas‘𝑌))
16		elfg 23989	. . . . . . . . . 10 ⊢ (𝐹 ∈ (fBas‘𝑌) → (𝑦 ∈ (𝑌filGen𝐹) ↔ (𝑦 ⊆ 𝑌 ∧ ∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦)))
17	15, 16	syl 18	. . . . . . . . 9 ⊢ ((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ 𝑥 ⊆ 𝑋) → (𝑦 ∈ (𝑌filGen𝐹) ↔ (𝑦 ⊆ 𝑌 ∧ ∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦)))
18		fbsspw 23950	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (fBas‘𝑌) → 𝐹 ⊆ 𝒫 𝑌)
19	1, 18	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝐹 ⊆ 𝒫 𝑌)
20	19, 8	sstrd 3949	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝐹 ⊆ 𝒫 𝑋)
21		fbasweak 23983	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝐹 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑋))
22	1, 20, 10, 21	syl3anc 1394	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑋))
23		fgcl 23996	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
24	22, 23	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
25	24	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ ((𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦) ∧ 𝑦 ⊆ 𝑥)) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
26		ssfg 23990	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (fBas‘𝑋) → 𝐹 ⊆ (𝑋filGen𝐹))
27	22, 26	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝐹 ⊆ (𝑋filGen𝐹))
28	27	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) → 𝐹 ⊆ (𝑋filGen𝐹))
29	28	sselda 3939	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ 𝑧 ∈ 𝐹) → 𝑧 ∈ (𝑋filGen𝐹))
30	29	adantrr 729	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ (𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦)) → 𝑧 ∈ (𝑋filGen𝐹))
31	30	adantrr 729	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ ((𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦) ∧ 𝑦 ⊆ 𝑥)) → 𝑧 ∈ (𝑋filGen𝐹))
32		simplrl 788	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ ((𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦) ∧ 𝑦 ⊆ 𝑥)) → 𝑥 ⊆ 𝑋)
33		simprlr 791	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ ((𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦) ∧ 𝑦 ⊆ 𝑥)) → 𝑧 ⊆ 𝑦)
34		simprr 784	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ ((𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦) ∧ 𝑦 ⊆ 𝑥)) → 𝑦 ⊆ 𝑥)
35	33, 34	sstrd 3949	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ ((𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦) ∧ 𝑦 ⊆ 𝑥)) → 𝑧 ⊆ 𝑥)
36		filss 23971	. . . . . . . . . . . . . 14 ⊢ (((𝑋filGen𝐹) ∈ (Fil‘𝑋) ∧ (𝑧 ∈ (𝑋filGen𝐹) ∧ 𝑥 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑥)) → 𝑥 ∈ (𝑋filGen𝐹))
37	25, 31, 32, 35, 36	syl13anc 1395	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ ((𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦) ∧ 𝑦 ⊆ 𝑥)) → 𝑥 ∈ (𝑋filGen𝐹))
38	37	expr 461	. . . . . . . . . . . 12 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ (𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦)) → (𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝑋filGen𝐹)))
39	38	rexlimdvaa 3167	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) → (∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦 → (𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝑋filGen𝐹))))
40	39	anassrs 472	. . . . . . . . . 10 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ 𝑥 ⊆ 𝑋) ∧ 𝑦 ⊆ 𝑌) → (∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦 → (𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝑋filGen𝐹))))
41	40	expimpd 458	. . . . . . . . 9 ⊢ ((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ 𝑥 ⊆ 𝑋) → ((𝑦 ⊆ 𝑌 ∧ ∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦) → (𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝑋filGen𝐹))))
42	17, 41	sylbid 243	. . . . . . . 8 ⊢ ((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ 𝑥 ⊆ 𝑋) → (𝑦 ∈ (𝑌filGen𝐹) → (𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝑋filGen𝐹))))
43	42	rexlimdv 3164	. . . . . . 7 ⊢ ((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ 𝑥 ⊆ 𝑋) → (∃𝑦 ∈ (𝑌filGen𝐹)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝑋filGen𝐹)))
44	43	expimpd 458	. . . . . 6 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → ((𝑥 ⊆ 𝑋 ∧ ∃𝑦 ∈ (𝑌filGen𝐹)𝑦 ⊆ 𝑥) → 𝑥 ∈ (𝑋filGen𝐹)))
45	14, 44	sylbid 243	. . . . 5 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑥 ∈ (𝑋filGen(𝑌filGen𝐹)) → 𝑥 ∈ (𝑋filGen𝐹)))
46	45	ssrdv 3945	. . . 4 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑋filGen(𝑌filGen𝐹)) ⊆ (𝑋filGen𝐹))
47		ssfg 23990	. . . . . 6 ⊢ (𝐹 ∈ (fBas‘𝑌) → 𝐹 ⊆ (𝑌filGen𝐹))
48	47	ad2antrr 738	. . . . 5 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝐹 ⊆ (𝑌filGen𝐹))
49		fgss 23991	. . . . 5 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ (𝑌filGen𝐹) ∈ (fBas‘𝑋) ∧ 𝐹 ⊆ (𝑌filGen𝐹)) → (𝑋filGen𝐹) ⊆ (𝑋filGen(𝑌filGen𝐹)))
50	22, 12, 48, 49	syl3anc 1394	. . . 4 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑋filGen𝐹) ⊆ (𝑋filGen(𝑌filGen𝐹)))
51	46, 50	eqssd 3956	. . 3 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹))
52	51	ex 417	. 2 ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) → (𝑋 ∈ V → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹)))
53		df-fg 21480	. . . . 5 ⊢ filGen = (𝑤 ∈ V, 𝑥 ∈ (fBas‘𝑤) ↦ {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅})
54	53	reldmmpo 7534	. . . 4 ⊢ Rel dom filGen
55	54	ovprc1 7439	. . 3 ⊢ (¬ 𝑋 ∈ V → (𝑋filGen(𝑌filGen𝐹)) = ∅)
56	54	ovprc1 7439	. . 3 ⊢ (¬ 𝑋 ∈ V → (𝑋filGen𝐹) = ∅)
57	55, 56	eqtr4d 2803	. 2 ⊢ (¬ 𝑋 ∈ V → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹))
58	52, 57	pm2.61d1 182	1 ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1563 ∈ wcel 2145 ≠ wne 2960 ∃wrex 3089 {crab 3417 Vcvv 3457 ∩ cin 3906 ⊆ wss 3907 ∅c0 4288 𝒫 cpw 4558 ‘cfv 6525 (class class class)co 7400 fBascfbas 21470 filGencfg 21471 Filcfil 23963

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5251 ax-nul 5261 ax-pow 5327 ax-pr 5395

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4869 df-br 5106 df-opab 5168 df-mpt 5187 df-id 5547 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-iota 6481 df-fun 6527 df-fv 6533 df-ov 7403 df-oprab 7404 df-mpo 7405 df-fbas 21479 df-fg 21480 df-fil 23964

This theorem is referenced by: minveclem4a 25550

W3C validator