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 23773

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 23772	. . . . . . . . 9 ⊢ (𝐹 ∈ (fBas‘𝑌) → (𝑌filGen𝐹) ∈ (Fil‘𝑌))
3		filfbas 23742	. . . . . . . . 9 ⊢ ((𝑌filGen𝐹) ∈ (Fil‘𝑌) → (𝑌filGen𝐹) ∈ (fBas‘𝑌))
4	1, 2, 3	3syl 18	. . . . . . . 8 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ∈ (fBas‘𝑌))
5		fbsspw 23726	. . . . . . . . . 10 ⊢ ((𝑌filGen𝐹) ∈ (fBas‘𝑌) → (𝑌filGen𝐹) ⊆ 𝒫 𝑌)
6	4, 5	syl 17	. . . . . . . . 9 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ⊆ 𝒫 𝑌)
7		simplr 768	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝑌 ⊆ 𝑋)
8	7	sspwd 4579	. . . . . . . . 9 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝒫 𝑌 ⊆ 𝒫 𝑋)
9	6, 8	sstrd 3960	. . . . . . . 8 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ⊆ 𝒫 𝑋)
10		simpr 484	. . . . . . . 8 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝑋 ∈ V)
11		fbasweak 23759	. . . . . . . 8 ⊢ (((𝑌filGen𝐹) ∈ (fBas‘𝑌) ∧ (𝑌filGen𝐹) ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ∈ (fBas‘𝑋))
12	4, 9, 10, 11	syl3anc 1373	. . . . . . 7 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ∈ (fBas‘𝑋))
13		elfg 23765	. . . . . . 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 23765	. . . . . . . . . 10 ⊢ (𝐹 ∈ (fBas‘𝑌) → (𝑦 ∈ (𝑌filGen𝐹) ↔ (𝑦 ⊆ 𝑌 ∧ ∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦)))
17	15, 16	syl 17	. . . . . . . . 9 ⊢ ((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ 𝑥 ⊆ 𝑋) → (𝑦 ∈ (𝑌filGen𝐹) ↔ (𝑦 ⊆ 𝑌 ∧ ∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦)))
18		fbsspw 23726	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (fBas‘𝑌) → 𝐹 ⊆ 𝒫 𝑌)
19	1, 18	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝐹 ⊆ 𝒫 𝑌)
20	19, 8	sstrd 3960	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝐹 ⊆ 𝒫 𝑋)
21		fbasweak 23759	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝐹 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑋))
22	1, 20, 10, 21	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑋))
23		fgcl 23772	. . . . . . . . . . . . . . . 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 23766	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (fBas‘𝑋) → 𝐹 ⊆ (𝑋filGen𝐹))
27	22, 26	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝐹 ⊆ (𝑋filGen𝐹))
28	27	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) → 𝐹 ⊆ (𝑋filGen𝐹))
29	28	sselda 3949	. . . . . . . . . . . . . . . 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 3960	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ ((𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦) ∧ 𝑦 ⊆ 𝑥)) → 𝑧 ⊆ 𝑥)
36		filss 23747	. . . . . . . . . . . . . 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 3136	. . . . . . . . . . 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 3133	. . . . . . 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 3955	. . . 4 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑋filGen(𝑌filGen𝐹)) ⊆ (𝑋filGen𝐹))
47		ssfg 23766	. . . . . 6 ⊢ (𝐹 ∈ (fBas‘𝑌) → 𝐹 ⊆ (𝑌filGen𝐹))
48	47	ad2antrr 726	. . . . 5 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝐹 ⊆ (𝑌filGen𝐹))
49		fgss 23767	. . . . 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 3967	. . 3 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹))
52	51	ex 412	. 2 ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) → (𝑋 ∈ V → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹)))
53		df-fg 21269	. . . . 5 ⊢ filGen = (𝑤 ∈ V, 𝑥 ∈ (fBas‘𝑤) ↦ {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅})
54	53	reldmmpo 7526	. . . 4 ⊢ Rel dom filGen
55	54	ovprc1 7429	. . 3 ⊢ (¬ 𝑋 ∈ V → (𝑋filGen(𝑌filGen𝐹)) = ∅)
56	54	ovprc1 7429	. . 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 1540 ∈ wcel 2109 ≠ wne 2926 ∃wrex 3054 {crab 3408 Vcvv 3450 ∩ cin 3916 ⊆ wss 3917 ∅c0 4299 𝒫 cpw 4566 ‘cfv 6514 (class class class)co 7390 fBascfbas 21259 filGencfg 21260 Filcfil 23739

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 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 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-br 5111 df-opab 5173 df-mpt 5192 df-id 5536 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-iota 6467 df-fun 6516 df-fv 6522 df-ov 7393 df-oprab 7394 df-mpo 7395 df-fbas 21268 df-fg 21269 df-fil 23740

This theorem is referenced by: minveclem4a 25337

W3C validator