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 23787

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 766	. . . . . . . . 9 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑌))
2		fgcl 23786	. . . . . . . . 9 ⊢ (𝐹 ∈ (fBas‘𝑌) → (𝑌filGen𝐹) ∈ (Fil‘𝑌))
3		filfbas 23756	. . . . . . . . 9 ⊢ ((𝑌filGen𝐹) ∈ (Fil‘𝑌) → (𝑌filGen𝐹) ∈ (fBas‘𝑌))
4	1, 2, 3	3syl 18	. . . . . . . 8 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ∈ (fBas‘𝑌))
5		fbsspw 23740	. . . . . . . . . 10 ⊢ ((𝑌filGen𝐹) ∈ (fBas‘𝑌) → (𝑌filGen𝐹) ⊆ 𝒫 𝑌)
6	4, 5	syl 17	. . . . . . . . 9 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ⊆ 𝒫 𝑌)
7		simplr 768	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝑌 ⊆ 𝑋)
8	7	sspwd 4561	. . . . . . . . 9 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝒫 𝑌 ⊆ 𝒫 𝑋)
9	6, 8	sstrd 3943	. . . . . . . 8 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ⊆ 𝒫 𝑋)
10		simpr 484	. . . . . . . 8 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝑋 ∈ V)
11		fbasweak 23773	. . . . . . . 8 ⊢ (((𝑌filGen𝐹) ∈ (fBas‘𝑌) ∧ (𝑌filGen𝐹) ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ∈ (fBas‘𝑋))
12	4, 9, 10, 11	syl3anc 1373	. . . . . . 7 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ∈ (fBas‘𝑋))
13		elfg 23779	. . . . . . 7 ⊢ ((𝑌filGen𝐹) ∈ (fBas‘𝑋) → (𝑥 ∈ (𝑋filGen(𝑌filGen𝐹)) ↔ (𝑥 ⊆ 𝑋 ∧ ∃𝑦 ∈ (𝑌filGen𝐹)𝑦 ⊆ 𝑥)))
14	12, 13	syl 17	. . . . . 6 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑥 ∈ (𝑋filGen(𝑌filGen𝐹)) ↔ (𝑥 ⊆ 𝑋 ∧ ∃𝑦 ∈ (𝑌filGen𝐹)𝑦 ⊆ 𝑥)))
15	1	adantr 480	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ 𝑥 ⊆ 𝑋) → 𝐹 ∈ (fBas‘𝑌))
16		elfg 23779	. . . . . . . . . 10 ⊢ (𝐹 ∈ (fBas‘𝑌) → (𝑦 ∈ (𝑌filGen𝐹) ↔ (𝑦 ⊆ 𝑌 ∧ ∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦)))
17	15, 16	syl 17	. . . . . . . . 9 ⊢ ((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ 𝑥 ⊆ 𝑋) → (𝑦 ∈ (𝑌filGen𝐹) ↔ (𝑦 ⊆ 𝑌 ∧ ∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦)))
18		fbsspw 23740	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (fBas‘𝑌) → 𝐹 ⊆ 𝒫 𝑌)
19	1, 18	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝐹 ⊆ 𝒫 𝑌)
20	19, 8	sstrd 3943	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝐹 ⊆ 𝒫 𝑋)
21		fbasweak 23773	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝐹 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑋))
22	1, 20, 10, 21	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑋))
23		fgcl 23786	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
24	22, 23	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
25	24	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ ((𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦) ∧ 𝑦 ⊆ 𝑥)) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
26		ssfg 23780	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (fBas‘𝑋) → 𝐹 ⊆ (𝑋filGen𝐹))
27	22, 26	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝐹 ⊆ (𝑋filGen𝐹))
28	27	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) → 𝐹 ⊆ (𝑋filGen𝐹))
29	28	sselda 3932	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ 𝑧 ∈ 𝐹) → 𝑧 ∈ (𝑋filGen𝐹))
30	29	adantrr 717	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ (𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦)) → 𝑧 ∈ (𝑋filGen𝐹))
31	30	adantrr 717	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ ((𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦) ∧ 𝑦 ⊆ 𝑥)) → 𝑧 ∈ (𝑋filGen𝐹))
32		simplrl 776	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ ((𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦) ∧ 𝑦 ⊆ 𝑥)) → 𝑥 ⊆ 𝑋)
33		simprlr 779	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ ((𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦) ∧ 𝑦 ⊆ 𝑥)) → 𝑧 ⊆ 𝑦)
34		simprr 772	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ ((𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦) ∧ 𝑦 ⊆ 𝑥)) → 𝑦 ⊆ 𝑥)
35	33, 34	sstrd 3943	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ ((𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦) ∧ 𝑦 ⊆ 𝑥)) → 𝑧 ⊆ 𝑥)
36		filss 23761	. . . . . . . . . . . . . 14 ⊢ (((𝑋filGen𝐹) ∈ (Fil‘𝑋) ∧ (𝑧 ∈ (𝑋filGen𝐹) ∧ 𝑥 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑥)) → 𝑥 ∈ (𝑋filGen𝐹))
37	25, 31, 32, 35, 36	syl13anc 1374	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ ((𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦) ∧ 𝑦 ⊆ 𝑥)) → 𝑥 ∈ (𝑋filGen𝐹))
38	37	expr 456	. . . . . . . . . . . 12 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ (𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦)) → (𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝑋filGen𝐹)))
39	38	rexlimdvaa 3132	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) → (∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦 → (𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝑋filGen𝐹))))
40	39	anassrs 467	. . . . . . . . . 10 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ 𝑥 ⊆ 𝑋) ∧ 𝑦 ⊆ 𝑌) → (∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦 → (𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝑋filGen𝐹))))
41	40	expimpd 453	. . . . . . . . 9 ⊢ ((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ 𝑥 ⊆ 𝑋) → ((𝑦 ⊆ 𝑌 ∧ ∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦) → (𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝑋filGen𝐹))))
42	17, 41	sylbid 240	. . . . . . . 8 ⊢ ((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ 𝑥 ⊆ 𝑋) → (𝑦 ∈ (𝑌filGen𝐹) → (𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝑋filGen𝐹))))
43	42	rexlimdv 3129	. . . . . . 7 ⊢ ((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ 𝑥 ⊆ 𝑋) → (∃𝑦 ∈ (𝑌filGen𝐹)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝑋filGen𝐹)))
44	43	expimpd 453	. . . . . 6 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → ((𝑥 ⊆ 𝑋 ∧ ∃𝑦 ∈ (𝑌filGen𝐹)𝑦 ⊆ 𝑥) → 𝑥 ∈ (𝑋filGen𝐹)))
45	14, 44	sylbid 240	. . . . 5 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑥 ∈ (𝑋filGen(𝑌filGen𝐹)) → 𝑥 ∈ (𝑋filGen𝐹)))
46	45	ssrdv 3938	. . . 4 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑋filGen(𝑌filGen𝐹)) ⊆ (𝑋filGen𝐹))
47		ssfg 23780	. . . . . 6 ⊢ (𝐹 ∈ (fBas‘𝑌) → 𝐹 ⊆ (𝑌filGen𝐹))
48	47	ad2antrr 726	. . . . 5 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝐹 ⊆ (𝑌filGen𝐹))
49		fgss 23781	. . . . 5 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ (𝑌filGen𝐹) ∈ (fBas‘𝑋) ∧ 𝐹 ⊆ (𝑌filGen𝐹)) → (𝑋filGen𝐹) ⊆ (𝑋filGen(𝑌filGen𝐹)))
50	22, 12, 48, 49	syl3anc 1373	. . . 4 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑋filGen𝐹) ⊆ (𝑋filGen(𝑌filGen𝐹)))
51	46, 50	eqssd 3950	. . 3 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹))
52	51	ex 412	. 2 ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) → (𝑋 ∈ V → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹)))
53		df-fg 21282	. . . . 5 ⊢ filGen = (𝑤 ∈ V, 𝑥 ∈ (fBas‘𝑤) ↦ {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅})
54	53	reldmmpo 7475	. . . 4 ⊢ Rel dom filGen
55	54	ovprc1 7380	. . 3 ⊢ (¬ 𝑋 ∈ V → (𝑋filGen(𝑌filGen𝐹)) = ∅)
56	54	ovprc1 7380	. . 3 ⊢ (¬ 𝑋 ∈ V → (𝑋filGen𝐹) = ∅)
57	55, 56	eqtr4d 2768	. 2 ⊢ (¬ 𝑋 ∈ V → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹))
58	52, 57	pm2.61d1 180	1 ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∈ wcel 2110 ≠ wne 2926 ∃wrex 3054 {crab 3393 Vcvv 3434 ∩ cin 3899 ⊆ wss 3900 ∅c0 4281 𝒫 cpw 4548 ‘cfv 6477 (class class class)co 7341 fBascfbas 21272 filGencfg 21273 Filcfil 23753

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2112 ax-9 2120 ax-10 2143 ax-11 2159 ax-12 2179 ax-ext 2702 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rab 3394 df-v 3436 df-sbc 3740 df-csb 3849 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-nul 4282 df-if 4474 df-pw 4550 df-sn 4575 df-pr 4577 df-op 4581 df-uni 4858 df-br 5090 df-opab 5152 df-mpt 5171 df-id 5509 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-iota 6433 df-fun 6479 df-fv 6485 df-ov 7344 df-oprab 7345 df-mpo 7346 df-fbas 21281 df-fg 21282 df-fil 23754

This theorem is referenced by: minveclem4a 25350

W3C validator