Theorem cnfilca 10451

Description: Condition to have a filter finer than a given filter and containing a set A. Bourbaki T.G. I.37 cor. 1

Assertion

Ref	Expression
cnfilca	⊢ ((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) → (∃g ∈ Fil (A ∈ g ⋀ F ⊆ g) ↔ ∀x ∈ F (x ∩ A) ≠ ∅))

Distinct variable groups:   A,g   x,A   g,F   x,F

Proof of Theorem cnfilca

Step	Hyp	Ref	Expression
1		ssexg 2711	. . . . . . 7 ⊢ ((A ⊆ ∪F ⋀ ∪F ∈ V) → A ∈ V)
2		uniexg 2862	. . . . . . 7 ⊢ (F ∈ Fil → ∪F ∈ V)
3	1, 2	sylan2 451	. . . . . 6 ⊢ ((A ⊆ ∪F ⋀ F ∈ Fil) → A ∈ V)
4	3	ancoms 436	. . . . 5 ⊢ ((F ∈ Fil ⋀ A ⊆ ∪F) → A ∈ V)
5	4	3adant3 797	. . . 4 ⊢ ((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) → A ∈ V)
6		snssg 2454	. . . . . 6 ⊢ (A ∈ V → (A ∈ g ↔ {A} ⊆ g))
7	6	anbi1d 615	. . . . 5 ⊢ (A ∈ V → ((A ∈ g ⋀ F ⊆ g) ↔ ({A} ⊆ g ⋀ F ⊆ g)))
8		unss 2194	. . . . 5 ⊢ (({A} ⊆ g ⋀ F ⊆ g) ↔ ({A} ∪ F) ⊆ g)
9	7, 8	syl6bb 534	. . . 4 ⊢ (A ∈ V → ((A ∈ g ⋀ F ⊆ g) ↔ ({A} ∪ F) ⊆ g))
10	5, 9	syl 10	. . 3 ⊢ ((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) → ((A ∈ g ⋀ F ⊆ g) ↔ ({A} ∪ F) ⊆ g))
11	10	rexbidv 1656	. 2 ⊢ ((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) → (∃g ∈ Fil (A ∈ g ⋀ F ⊆ g) ↔ ∃g ∈ Fil ({A} ∪ F) ⊆ g))
12		efilcp2 10450	. . 3 ⊢ ((({A} ∪ F) ⊆ ℘∪F ⋀ ∪F ∈ V ⋀ ({A} ∪ F) ≠ ∅) → (¬ ∅ ∈ (fi ‘({A} ∪ F)) ↔ ∃g ∈ Fil ({A} ∪ F) ⊆ g))
13	1	ex 373	. . . . . . 7 ⊢ (A ⊆ ∪F → (∪F ∈ V → A ∈ V))
14		elpwg 2395	. . . . . . . . 9 ⊢ (A ∈ V → (A ∈ ℘∪F ↔ A ⊆ ∪F))
15		snssg 2454	. . . . . . . . 9 ⊢ (A ∈ V → (A ∈ ℘∪F ↔ {A} ⊆ ℘∪F))
16	14, 15	bitr3d 528	. . . . . . . 8 ⊢ (A ∈ V → (A ⊆ ∪F ↔ {A} ⊆ ℘∪F))
17		pwuni 2747	. . . . . . . . 9 ⊢ F ⊆ ℘∪F
18		unss 2194	. . . . . . . . . 10 ⊢ (({A} ⊆ ℘∪F ⋀ F ⊆ ℘∪F) ↔ ({A} ∪ F) ⊆ ℘∪F)
19	18	biimp 151	. . . . . . . . 9 ⊢ (({A} ⊆ ℘∪F ⋀ F ⊆ ℘∪F) → ({A} ∪ F) ⊆ ℘∪F)
20	17, 19	mpan2 694	. . . . . . . 8 ⊢ ({A} ⊆ ℘∪F → ({A} ∪ F) ⊆ ℘∪F)
21	16, 20	syl6bi 214	. . . . . . 7 ⊢ (A ∈ V → (A ⊆ ∪F → ({A} ∪ F) ⊆ ℘∪F))
22	13, 21	syl6 22	. . . . . 6 ⊢ (A ⊆ ∪F → (∪F ∈ V → (A ⊆ ∪F → ({A} ∪ F) ⊆ ℘∪F)))
23	22	pm2.43a 66	. . . . 5 ⊢ (A ⊆ ∪F → (∪F ∈ V → ({A} ∪ F) ⊆ ℘∪F))
24	2, 23	mpan9 470	. . . 4 ⊢ ((F ∈ Fil ⋀ A ⊆ ∪F) → ({A} ∪ F) ⊆ ℘∪F)
25	24	3adant3 797	. . 3 ⊢ ((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) → ({A} ∪ F) ⊆ ℘∪F)
26	2	3ad2ant1 798	. . 3 ⊢ ((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) → ∪F ∈ V)
27		emnfil 10440	. . . . 5 ⊢ ¬ ∅ ∈ Fil
28		nelneq 1553	. . . . . 6 ⊢ ((F ∈ Fil ⋀ ¬ ∅ ∈ Fil) → ¬ F = ∅)
29		pm3.27 323	. . . . . . . 8 ⊢ (({A} = ∅ ⋀ F = ∅) → F = ∅)
30	29	con3i 98	. . . . . . 7 ⊢ (¬ F = ∅ → ¬ ({A} = ∅ ⋀ F = ∅))
31		un00 2296	. . . . . . . 8 ⊢ (({A} = ∅ ⋀ F = ∅) ↔ ({A} ∪ F) = ∅)
32	31	necon3bbii 1589	. . . . . . 7 ⊢ (¬ ({A} = ∅ ⋀ F = ∅) ↔ ({A} ∪ F) ≠ ∅)
33	30, 32	sylib 198	. . . . . 6 ⊢ (¬ F = ∅ → ({A} ∪ F) ≠ ∅)
34	28, 33	syl 10	. . . . 5 ⊢ ((F ∈ Fil ⋀ ¬ ∅ ∈ Fil) → ({A} ∪ F) ≠ ∅)
35	27, 34	mpan2 694	. . . 4 ⊢ (F ∈ Fil → ({A} ∪ F) ≠ ∅)
36	35	3ad2ant1 798	. . 3 ⊢ ((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) → ({A} ∪ F) ≠ ∅)
37	12, 25, 26, 36	syl3anc 856	. 2 ⊢ ((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) → (¬ ∅ ∈ (fi ‘({A} ∪ F)) ↔ ∃g ∈ Fil ({A} ∪ F) ⊆ g))
38		elisset 1808	. . . . . . . 8 ⊢ (F ∈ Fil → F ∈ V)
39	38	3ad2ant1 798	. . . . . . 7 ⊢ ((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) → F ∈ V)
40		snex 2740	. . . . . . 7 ⊢ {A} ∈ V
41	39, 40	jctil 292	. . . . . 6 ⊢ ((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) → ({A} ∈ V ⋀ F ∈ V))
42		unexb 2864	. . . . . 6 ⊢ (({A} ∈ V ⋀ F ∈ V) ↔ ({A} ∪ F) ∈ V)
43	41, 42	sylib 198	. . . . 5 ⊢ ((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) → ({A} ∪ F) ∈ V)
44		0ex 2701	. . . . 5 ⊢ ∅ ∈ V
45	43, 44	jctil 292	. . . 4 ⊢ ((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) → (∅ ∈ V ⋀ ({A} ∪ F) ∈ V))
46		sppfi 10376	. . . . 5 ⊢ ((∅ ∈ V ⋀ ({A} ∪ F) ∈ V) → (∅ ∈ (fi ‘({A} ∪ F)) ↔ ∃y(y ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω y ≈ u ⋀ ∅ = ∩y)))
47	46	negbid 609	. . . 4 ⊢ ((∅ ∈ V ⋀ ({A} ∪ F) ∈ V) → (¬ ∅ ∈ (fi ‘({A} ∪ F)) ↔ ¬ ∃y(y ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω y ≈ u ⋀ ∅ = ∩y)))
48	45, 47	syl 10	. . 3 ⊢ ((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) → (¬ ∅ ∈ (fi ‘({A} ∪ F)) ↔ ¬ ∃y(y ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω y ≈ u ⋀ ∅ = ∩y)))
49		ax-17 968	. . . . . 6 ⊢ (((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ ∀y((y ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω y ≈ u) → ¬ ∅ = ∩y)) → ∀x((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ ∀y((y ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω y ≈ u) → ¬ ∅ = ∩y)))
50		elun2 2188	. . . . . . . . . . . . . . . . . 18 ⊢ (x ∈ F → x ∈ ({A} ∪ F))
51	50	adantl 388	. . . . . . . . . . . . . . . . 17 ⊢ (((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ x ∈ F) → x ∈ ({A} ∪ F))
52		snidg 2423	. . . . . . . . . . . . . . . . . . . 20 ⊢ (A ∈ V → A ∈ {A})
53		elun1 2187	. . . . . . . . . . . . . . . . . . . 20 ⊢ (A ∈ {A} → A ∈ ({A} ∪ F))
54	52, 53	syl 10	. . . . . . . . . . . . . . . . . . 19 ⊢ (A ∈ V → A ∈ ({A} ∪ F))
55	5, 54	syl 10	. . . . . . . . . . . . . . . . . 18 ⊢ ((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) → A ∈ ({A} ∪ F))
56	55	adantr 389	. . . . . . . . . . . . . . . . 17 ⊢ (((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ x ∈ F) → A ∈ ({A} ∪ F))
57	51, 56	jca 288	. . . . . . . . . . . . . . . 16 ⊢ (((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ x ∈ F) → (x ∈ ({A} ∪ F) ⋀ A ∈ ({A} ∪ F)))
58		prssg 2463	. . . . . . . . . . . . . . . . . 18 ⊢ ((x ∈ F ⋀ A ∈ ℘∪F) → ((x ∈ ({A} ∪ F) ⋀ A ∈ ({A} ∪ F)) ↔ {x, A} ⊆ ({A} ∪ F)))
59	58	bicomd 519	. . . . . . . . . . . . . . . . 17 ⊢ ((x ∈ F ⋀ A ∈ ℘∪F) → ({x, A} ⊆ ({A} ∪ F) ↔ (x ∈ ({A} ∪ F) ⋀ A ∈ ({A} ∪ F))))
60		pm3.27 323	. . . . . . . . . . . . . . . . 17 ⊢ (((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ x ∈ F) → x ∈ F)
61		3simp2 787	. . . . . . . . . . . . . . . . . . 19 ⊢ ((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) → A ⊆ ∪F)
62	5, 14	syl 10	. . . . . . . . . . . . . . . . . . 19 ⊢ ((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) → (A ∈ ℘∪F ↔ A ⊆ ∪F))
63	61, 62	mpbird 196	. . . . . . . . . . . . . . . . . 18 ⊢ ((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) → A ∈ ℘∪F)
64	63	adantr 389	. . . . . . . . . . . . . . . . 17 ⊢ (((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ x ∈ F) → A ∈ ℘∪F)
65	59, 60, 64	sylanc 471	. . . . . . . . . . . . . . . 16 ⊢ (((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ x ∈ F) → ({x, A} ⊆ ({A} ∪ F) ↔ (x ∈ ({A} ∪ F) ⋀ A ∈ ({A} ∪ F))))
66	57, 65	mpbird 196	. . . . . . . . . . . . . . 15 ⊢ (((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ x ∈ F) → {x, A} ⊆ ({A} ∪ F))
67		prfi 4531	. . . . . . . . . . . . . . 15 ⊢ ∃u ∈ ω {x, A} ≈ u
68	66, 67	jctir 293	. . . . . . . . . . . . . 14 ⊢ (((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ x ∈ F) → ({x, A} ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω {x, A} ≈ u))
69		prex 2771	. . . . . . . . . . . . . . . 16 ⊢ {x, A} ∈ V
70	69	a1i 8	. . . . . . . . . . . . . . 15 ⊢ (((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ x ∈ F) → {x, A} ∈ V)
71		sseq1 2072	. . . . . . . . . . . . . . . . . 18 ⊢ (y = {x, A} → (y ⊆ ({A} ∪ F) ↔ {x, A} ⊆ ({A} ∪ F)))
72		breq1 2612	. . . . . . . . . . . . . . . . . . 19 ⊢ (y = {x, A} → (y ≈ u ↔ {x, A} ≈ u))
73	72	rexbidv 1656	. . . . . . . . . . . . . . . . . 18 ⊢ (y = {x, A} → (∃u ∈ ω y ≈ u ↔ ∃u ∈ ω {x, A} ≈ u))
74	71, 73	anbi12d 626	. . . . . . . . . . . . . . . . 17 ⊢ (y = {x, A} → ((y ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω y ≈ u) ↔ ({x, A} ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω {x, A} ≈ u)))
75		inteq 2526	. . . . . . . . . . . . . . . . . . 19 ⊢ (y = {x, A} → ∩y = ∩{x, A})
76	75	eqeq2d 1478	. . . . . . . . . . . . . . . . . 18 ⊢ (y = {x, A} → (∅ = ∩y ↔ ∅ = ∩{x, A}))
77	76	negbid 609	. . . . . . . . . . . . . . . . 17 ⊢ (y = {x, A} → (¬ ∅ = ∩y ↔ ¬ ∅ = ∩{x, A}))
78	74, 77	imbi12d 624	. . . . . . . . . . . . . . . 16 ⊢ (y = {x, A} → (((y ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω y ≈ u) → ¬ ∅ = ∩y) ↔ (({x, A} ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω {x, A} ≈ u) → ¬ ∅ = ∩{x, A})))
79	78	cla4gv 1853	. . . . . . . . . . . . . . 15 ⊢ ({x, A} ∈ V → (∀y((y ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω y ≈ u) → ¬ ∅ = ∩y) → (({x, A} ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω {x, A} ≈ u) → ¬ ∅ = ∩{x, A})))
80	70, 79	syl 10	. . . . . . . . . . . . . 14 ⊢ (((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ x ∈ F) → (∀y((y ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω y ≈ u) → ¬ ∅ = ∩y) → (({x, A} ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω {x, A} ≈ u) → ¬ ∅ = ∩{x, A})))
81	68, 80	mpid 47	. . . . . . . . . . . . 13 ⊢ (((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ x ∈ F) → (∀y((y ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω y ≈ u) → ¬ ∅ = ∩y) → ¬ ∅ = ∩{x, A}))
82	81	ex 373	. . . . . . . . . . . 12 ⊢ ((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) → (x ∈ F → (∀y((y ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω y ≈ u) → ¬ ∅ = ∩y) → ¬ ∅ = ∩{x, A})))
83	82	com23 32	. . . . . . . . . . 11 ⊢ ((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) → (∀y((y ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω y ≈ u) → ¬ ∅ = ∩y) → (x ∈ F → ¬ ∅ = ∩{x, A})))
84	83	imp31 362	. . . . . . . . . 10 ⊢ ((((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ ∀y((y ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω y ≈ u) → ¬ ∅ = ∩y)) ⋀ x ∈ F) → ¬ ∅ = ∩{x, A})
85		df-ne 1579	. . . . . . . . . 10 ⊢ (∅ ≠ ∩{x, A} ↔ ¬ ∅ = ∩{x, A})
86	84, 85	sylibr 200	. . . . . . . . 9 ⊢ ((((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ ∀y((y ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω y ≈ u) → ¬ ∅ = ∩y)) ⋀ x ∈ F) → ∅ ≠ ∩{x, A})
87	86	necomd 1629	. . . . . . . 8 ⊢ ((((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ ∀y((y ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω y ≈ u) → ¬ ∅ = ∩y)) ⋀ x ∈ F) → ∩{x, A} ≠ ∅)
88	5	ad2antrr 404	. . . . . . . . . . . 12 ⊢ ((((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ ∀y((y ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω y ≈ u) → ¬ ∅ = ∩y)) ⋀ x ∈ F) → A ∈ V)
89		visset 1804	. . . . . . . . . . . 12 ⊢ x ∈ V
90	88, 89	jctil 292	. . . . . . . . . . 11 ⊢ ((((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ ∀y((y ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω y ≈ u) → ¬ ∅ = ∩y)) ⋀ x ∈ F) → (x ∈ V ⋀ A ∈ V))
91		intprd 10367	. . . . . . . . . . 11 ⊢ ((x ∈ V ⋀ A ∈ V) → ∩{x, A} = (x ∩ A))
92	90, 91	syl 10	. . . . . . . . . 10 ⊢ ((((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ ∀y((y ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω y ≈ u) → ¬ ∅ = ∩y)) ⋀ x ∈ F) → ∩{x, A} = (x ∩ A))
93	92	eqcomd 1472	. . . . . . . . 9 ⊢ ((((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ ∀y((y ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω y ≈ u) → ¬ ∅ = ∩y)) ⋀ x ∈ F) → (x ∩ A) = ∩{x, A})
94	93	neeq1d 1586	. . . . . . . 8 ⊢ ((((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ ∀y((y ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω y ≈ u) → ¬ ∅ = ∩y)) ⋀ x ∈ F) → ((x ∩ A) ≠ ∅ ↔ ∩{x, A} ≠ ∅))
95	87, 94	mpbird 196	. . . . . . 7 ⊢ ((((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ ∀y((y ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω y ≈ u) → ¬ ∅ = ∩y)) ⋀ x ∈ F) → (x ∩ A) ≠ ∅)
96	95	ex 373	. . . . . 6 ⊢ (((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ ∀y((y ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω y ≈ u) → ¬ ∅ = ∩y)) → (x ∈ F → (x ∩ A) ≠ ∅))
97	49, 96	r19.21ai 1704	. . . . 5 ⊢ (((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ ∀y((y ⊆ ({A} ∪ F) ⋀ ∃u ∈ ω y ≈ u) → ¬ ∅ = ∩y)) → ∀x ∈ F (x ∩ A) ≠ ∅)
98		moec 10357	. . . . . . . 8 ⊢ (A ∈ y → ∩y = (A ∩ ∩(y ∖ {A})))
99		ssundif 2334	. . . . . . . . . . 11 ⊢ (y ⊆ ({A} ∪ F) ↔ (y ∖ {A}) ⊆ F)
100		inteq 2526	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((y ∖ {A}) = ∅ → ∩(y ∖ {A}) = ∩∅)
101		int0 2537	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∩∅ = V
102		eqtrt 1484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((∩(y ∖ {A}) = ∩∅ ⋀ ∩∅ = V) → ∩(y ∖ {A}) = V)
103	102	ex 373	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∩(y ∖ {A}) = ∩∅ → (∩∅ = V → ∩(y ∖ {A}) = V))
104		ineq2 2201	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∩(y ∖ {A}) = V → (A ∩ ∩(y ∖ {A})) = (A ∩ V))
105		inv1 2289	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (A ∩ V) = A
106		eqtrt 1484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((A ∩ ∩(y ∖ {A})) = (A ∩ V) ⋀ (A ∩ V) = A) → (A ∩ ∩(y ∖ {A})) = A)
107	106	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((A ∩ ∩(y ∖ {A})) = (A ∩ V) → ((A ∩ V) = A → (A ∩ ∩(y ∖ {A})) = A))
108		eqtrt 1484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((∩y = (A ∩ ∩(y ∖ {A})) ⋀ (A ∩ ∩(y ∖ {A})) = A) → ∩y = A)
109	108	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∩y = (A ∩ ∩(y ∖ {A})) → ((A ∩ ∩(y ∖ {A})) = A → ∩y = A))
110		neeq1 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (A = ∩y → (A ≠ ∅ ↔ ∩y ≠ ∅))
111		necom 1628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∩y ≠ ∅ ↔ ∅ ≠ ∩y)
112		df-ne 1579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∅ ≠ ∩y ↔ ¬ ∅ = ∩y)
113	112	biimp 151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∅ ≠ ∩y → ¬ ∅ = ∩y)
114	111, 113	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∩y ≠ ∅ → ¬ ∅ = ∩y)
115	110, 114	syl6bi 214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (A = ∩y → (A ≠ ∅ → ¬ ∅ = ∩y))
116	115	eqcoms 1470	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∩y = A → (A ≠ ∅ → ¬ ∅ = ∩y))
117	109, 116	syl6 22	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∩y = (A ∩ ∩(y ∖ {A})) → ((A ∩ ∩(y ∖ {A})) = A → (A ≠ ∅ → ¬ ∅ = ∩y)))
118	117	com3l 34	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((A ∩ ∩(y ∖ {A})) = A → (A ≠ ∅ → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y)))
119	107, 118	syl6 22	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((A ∩ ∩(y ∖ {A})) = (A ∩ V) → ((A ∩ V) = A → (A ≠ ∅ → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y))))
120	105, 119	mpi 44	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((A ∩ ∩(y ∖ {A})) = (A ∩ V) → (A ≠ ∅ → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y)))
121	104, 120	syl 10	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∩(y ∖ {A}) = V → (A ≠ ∅ → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y)))
122	103, 121	syl6com 53	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∩∅ = V → (∩(y ∖ {A}) = ∩∅ → (A ≠ ∅ → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y))))
123	101, 122	ax-mp 7	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∩(y ∖ {A}) = ∩∅ → (A ≠ ∅ → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y)))
124	100, 123	syl 10	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y ∖ {A}) = ∅ → (A ≠ ∅ → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y)))
125	124	com12 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (A ≠ ∅ → ((y ∖ {A}) = ∅ → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y)))
126	125	a1i 8	. . . . . . . . . . . . . . . . . 18 ⊢ ((y ∖ {A}) ⊆ F → (A ≠ ∅ → ((y ∖ {A}) = ∅ → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y))))
127	126	a1i 8	. . . . . . . . . . . . . . . . 17 ⊢ (∀x ∈ F (x ∩ A) ≠ ∅ → ((y ∖ {A}) ⊆ F → (A ≠ ∅ → ((y ∖ {A}) = ∅ → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y)))))
128	127	a1i 8	. . . . . . . . . . . . . . . 16 ⊢ (∃u ∈ ω y ≈ u → (∀x ∈ F (x ∩ A) ≠ ∅ → ((y ∖ {A}) ⊆ F → (A ≠ ∅ → ((y ∖ {A}) = ∅ → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y))))))
129	128	com14 38	. . . . . . . . . . . . . . 15 ⊢ (A ≠ ∅ → (∀x ∈ F (x ∩ A) ≠ ∅ → ((y ∖ {A}) ⊆ F → (∃u ∈ ω y ≈ u → ((y ∖ {A}) = ∅ → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y))))))
130	129	3ad2ant3 800	. . . . . . . . . . . . . 14 ⊢ ((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) → (∀x ∈ F (x ∩ A) ≠ ∅ → ((y ∖ {A}) ⊆ F → (∃u ∈ ω y ≈ u → ((y ∖ {A}) = ∅ → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y))))))
131	130	imp 350	. . . . . . . . . . . . 13 ⊢ (((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ ∀x ∈ F (x ∩ A) ≠ ∅) → ((y ∖ {A}) ⊆ F → (∃u ∈ ω y ≈ u → ((y ∖ {A}) = ∅ → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y)))))
132	131	com14 38	. . . . . . . . . . . 12 ⊢ ((y ∖ {A}) = ∅ → ((y ∖ {A}) ⊆ F → (∃u ∈ ω y ≈ u → (((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) ⋀ ∀x ∈ F (x ∩ A) ≠ ∅) → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y)))))
133		difss 2157	. . . . . . . . . . . . 13 ⊢ (y ∖ {A}) ⊆ y
134		ssfi 4515	. . . . . . . . . . . . . . . 16 ⊢ ((∃u ∈ ω y ≈ u ⋀ (y ∖ {A}) ⊆ y) → ∃u ∈ ω (y ∖ {A}) ≈ u)
135	134	ex 373	. . . . . . . . . . . . . . 15 ⊢ (∃u ∈ ω y ≈ u → ((y ∖ {A}) ⊆ y → ∃u ∈ ω (y ∖ {A}) ≈ u))
136		3simp1 786	. . . . . . . . . . . . . . . . 17 ⊢ ((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) → F ∈ Fil)
137		df-ne 1579	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((y ∖ {A}) ≠ ∅ ↔ ¬ (y ∖ {A}) = ∅)
138		filint2 10446	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (F ∈ Fil → (((y ∖ {A}) ⊆ F ⋀ (y ∖ {A}) ≠ ∅ ⋀ ∃u ∈ ω (y ∖ {A}) ≈ u) → ∩(y ∖ {A}) ∈ F))
139		ineq1 2200	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (x = ∩(y ∖ {A}) → (x ∩ A) = (∩(y ∖ {A}) ∩ A))
140	139	neeq1d 1586	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (x = ∩(y ∖ {A}) → ((x ∩ A) ≠ ∅ ↔ (∩(y ∖ {A}) ∩ A) ≠ ∅))
141	140	rcla4v 1864	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∩(y ∖ {A}) ∈ F → (∀x ∈ F (x ∩ A) ≠ ∅ → (∩(y ∖ {A}) ∩ A) ≠ ∅))
142		incom 2198	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∩(y ∖ {A}) ∩ A) = (A ∩ ∩(y ∖ {A}))
143		neeq1 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((∩(y ∖ {A}) ∩ A) = (A ∩ ∩(y ∖ {A})) → ((∩(y ∖ {A}) ∩ A) ≠ ∅ ↔ (A ∩ ∩(y ∖ {A})) ≠ ∅))
144		neeq1 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((A ∩ ∩(y ∖ {A})) = ∩y → ((A ∩ ∩(y ∖ {A})) ≠ ∅ ↔ ∩y ≠ ∅))
145	144	biimpd 153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((A ∩ ∩(y ∖ {A})) = ∩y → ((A ∩ ∩(y ∖ {A})) ≠ ∅ → ∩y ≠ ∅))
146	145	eqcoms 1470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (∩y = (A ∩ ∩(y ∖ {A})) → ((A ∩ ∩(y ∖ {A})) ≠ ∅ → ∩y ≠ ∅))
147	146, 114	syl6com 53	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((A ∩ ∩(y ∖ {A})) ≠ ∅ → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y))
148	143, 147	syl6bi 214	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∩(y ∖ {A}) ∩ A) = (A ∩ ∩(y ∖ {A})) → ((∩(y ∖ {A}) ∩ A) ≠ ∅ → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y)))
149	142, 148	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((∩(y ∖ {A}) ∩ A) ≠ ∅ → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y))
150	141, 149	syl6 22	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∩(y ∖ {A}) ∈ F → (∀x ∈ F (x ∩ A) ≠ ∅ → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y)))
151	138, 150	syl6 22	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (F ∈ Fil → (((y ∖ {A}) ⊆ F ⋀ (y ∖ {A}) ≠ ∅ ⋀ ∃u ∈ ω (y ∖ {A}) ≈ u) → (∀x ∈ F (x ∩ A) ≠ ∅ → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y))))
152	151	3expd 848	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (F ∈ Fil → ((y ∖ {A}) ⊆ F → ((y ∖ {A}) ≠ ∅ → (∃u ∈ ω (y ∖ {A}) ≈ u → (∀x ∈ F (x ∩ A) ≠ ∅ → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y))))))
153	152	com13 33	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((y ∖ {A}) ≠ ∅ → ((y ∖ {A}) ⊆ F → (F ∈ Fil → (∃u ∈ ω (y ∖ {A}) ≈ u → (∀x ∈ F (x ∩ A) ≠ ∅ → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y))))))
154	137, 153	sylbir 201	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (y ∖ {A}) = ∅ → ((y ∖ {A}) ⊆ F → (F ∈ Fil → (∃u ∈ ω (y ∖ {A}) ≈ u → (∀x ∈ F (x ∩ A) ≠ ∅ → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y))))))
155	154	com13 33	. . . . . . . . . . . . . . . . . . . 20 ⊢ (F ∈ Fil → ((y ∖ {A}) ⊆ F → (¬ (y ∖ {A}) = ∅ → (∃u ∈ ω (y ∖ {A}) ≈ u → (∀x ∈ F (x ∩ A) ≠ ∅ → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y))))))
156	155	3imp 825	. . . . . . . . . . . . . . . . . . 19 ⊢ ((F ∈ Fil ⋀ (y ∖ {A}) ⊆ F ⋀ ¬ (y ∖ {A}) = ∅) → (∃u ∈ ω (y ∖ {A}) ≈ u → (∀x ∈ F (x ∩ A) ≠ ∅ → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y))))
157	156	com3r 35	. . . . . . . . . . . . . . . . . 18 ⊢ (∀x ∈ F (x ∩ A) ≠ ∅ → ((F ∈ Fil ⋀ (y ∖ {A}) ⊆ F ⋀ ¬ (y ∖ {A}) = ∅) → (∃u ∈ ω (y ∖ {A}) ≈ u → (∩y = (A ∩ ∩(y ∖ {A})) → ¬ ∅ = ∩y))))
158	157	3expd 848	. . . . . . . . . . . . . . . . 17 ⊢ (∀x ∈ F (x ∩ A) ≠ ∅ → (F ∈ Fil → ((y ∖ {A}) ⊆ F