Theorem fgsb2 10449

Description: Filter generated by a subbasis A. Bourbaki TG I.37 paragraph above prop. 1. (The theorem has been slightly modified because the definitions of the empty set are different in Bourbaki and Metamath.)

Assertion

Ref	Expression
fgsb2	⊢ ((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) → (¬ ∅ ∈ (fi ‘A) → {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ∈ Fil))

Distinct variable groups:   y,A,x   x,X,y

Proof of Theorem fgsb2

Step	Hyp	Ref	Expression
1		sseq2 2073	. . . . . . . . . 10 ⊢ (x = ∅ → (y ⊆ x ↔ y ⊆ ∅))
2	1	rexbidv 1656	. . . . . . . . 9 ⊢ (x = ∅ → (∃y ∈ (fi ‘A)y ⊆ x ↔ ∃y ∈ (fi ‘A)y ⊆ ∅))
3	2	elrab 1896	. . . . . . . 8 ⊢ (∅ ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ↔ (∅ ∈ ℘X ⋀ ∃y ∈ (fi ‘A)y ⊆ ∅))
4		ss0 2293	. . . . . . . . . . . 12 ⊢ (y ⊆ ∅ → y = ∅)
5	4	eleq1d 1532	. . . . . . . . . . 11 ⊢ (y ⊆ ∅ → (y ∈ (fi ‘A) ↔ ∅ ∈ (fi ‘A)))
6	5	biimpcd 155	. . . . . . . . . 10 ⊢ (y ∈ (fi ‘A) → (y ⊆ ∅ → ∅ ∈ (fi ‘A)))
7	6	r19.23aiv 1735	. . . . . . . . 9 ⊢ (∃y ∈ (fi ‘A)y ⊆ ∅ → ∅ ∈ (fi ‘A))
8	7	adantl 388	. . . . . . . 8 ⊢ ((∅ ∈ ℘X ⋀ ∃y ∈ (fi ‘A)y ⊆ ∅) → ∅ ∈ (fi ‘A))
9	3, 8	sylbi 199	. . . . . . 7 ⊢ (∅ ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} → ∅ ∈ (fi ‘A))
10	9	con3i 98	. . . . . 6 ⊢ (¬ ∅ ∈ (fi ‘A) → ¬ ∅ ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x})
11	10	adantl 388	. . . . 5 ⊢ (((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) ⋀ ¬ ∅ ∈ (fi ‘A)) → ¬ ∅ ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x})
12		ump 10355	. . . . . . . . 9 ⊢ (X ∈ V → ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ∈ ℘X)
13	12	3ad2ant2 799	. . . . . . . 8 ⊢ ((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) → ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ∈ ℘X)
14		r19.2z 2337	. . . . . . . . 9 ⊢ (((fi ‘A) ≠ ∅ ⋀ ∀y ∈ (fi ‘A)y ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x}) → ∃y ∈ (fi ‘A)y ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x})
15		fine2 10375	. . . . . . . . . 10 ⊢ (A ∈ V → (A ≠ ∅ → (fi ‘A) ≠ ∅))
16		ssexg 2711	. . . . . . . . . . 11 ⊢ ((A ⊆ ℘X ⋀ ℘X ∈ V) → A ∈ V)
17		3simp1 786	. . . . . . . . . . 11 ⊢ ((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) → A ⊆ ℘X)
18		pwexg 2736	. . . . . . . . . . . 12 ⊢ (X ∈ V → ℘X ∈ V)
19	18	3ad2ant2 799	. . . . . . . . . . 11 ⊢ ((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) → ℘X ∈ V)
20	16, 17, 19	sylanc 471	. . . . . . . . . 10 ⊢ ((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) → A ∈ V)
21		3simp3 788	. . . . . . . . . 10 ⊢ ((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) → A ≠ ∅)
22	15, 20, 21	sylc 68	. . . . . . . . 9 ⊢ ((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) → (fi ‘A) ≠ ∅)
23		fiiu2 10377	. . . . . . . . . . . . . . . . . . 19 ⊢ (A ∈ V → (y ∈ (fi ‘A) → y ⊆ ∪A))
24	16, 23	syl 10	. . . . . . . . . . . . . . . . . 18 ⊢ ((A ⊆ ℘X ⋀ ℘X ∈ V) → (y ∈ (fi ‘A) → y ⊆ ∪A))
25	24, 17, 19	sylanc 471	. . . . . . . . . . . . . . . . 17 ⊢ ((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) → (y ∈ (fi ‘A) → y ⊆ ∪A))
26	25	imp 350	. . . . . . . . . . . . . . . 16 ⊢ (((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) ⋀ y ∈ (fi ‘A)) → y ⊆ ∪A)
27		sspwuni 2748	. . . . . . . . . . . . . . . . . 18 ⊢ (A ⊆ ℘X ↔ ∪A ⊆ X)
28	17, 27	sylib 198	. . . . . . . . . . . . . . . . 17 ⊢ ((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) → ∪A ⊆ X)
29	28	adantr 389	. . . . . . . . . . . . . . . 16 ⊢ (((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) ⋀ y ∈ (fi ‘A)) → ∪A ⊆ X)
30	26, 29	sstrd 2064	. . . . . . . . . . . . . . 15 ⊢ (((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) ⋀ y ∈ (fi ‘A)) → y ⊆ X)
31		visset 1804	. . . . . . . . . . . . . . . 16 ⊢ y ∈ V
32	31	elpw 2394	. . . . . . . . . . . . . . 15 ⊢ (y ∈ ℘X ↔ y ⊆ X)
33	30, 32	sylibr 200	. . . . . . . . . . . . . 14 ⊢ (((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) ⋀ y ∈ (fi ‘A)) → y ∈ ℘X)
34		pm3.27 323	. . . . . . . . . . . . . . . 16 ⊢ (((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) ⋀ y ∈ (fi ‘A)) → y ∈ (fi ‘A))
35		ssid 2070	. . . . . . . . . . . . . . . 16 ⊢ y ⊆ y
36	34, 35	jctir 293	. . . . . . . . . . . . . . 15 ⊢ (((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) ⋀ y ∈ (fi ‘A)) → (y ∈ (fi ‘A) ⋀ y ⊆ y))
37		sseq1 2072	. . . . . . . . . . . . . . . 16 ⊢ (z = y → (z ⊆ y ↔ y ⊆ y))
38	37	rcla4ev 1868	. . . . . . . . . . . . . . 15 ⊢ ((y ∈ (fi ‘A) ⋀ y ⊆ y) → ∃z ∈ (fi ‘A)z ⊆ y)
39	36, 38	syl 10	. . . . . . . . . . . . . 14 ⊢ (((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) ⋀ y ∈ (fi ‘A)) → ∃z ∈ (fi ‘A)z ⊆ y)
40	33, 39	jca 288	. . . . . . . . . . . . 13 ⊢ (((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) ⋀ y ∈ (fi ‘A)) → (y ∈ ℘X ⋀ ∃z ∈ (fi ‘A)z ⊆ y))
41		sseq2 2073	. . . . . . . . . . . . . . . 16 ⊢ (x = y → (z ⊆ x ↔ z ⊆ y))
42	41	rexbidv 1656	. . . . . . . . . . . . . . 15 ⊢ (x = y → (∃z ∈ (fi ‘A)z ⊆ x ↔ ∃z ∈ (fi ‘A)z ⊆ y))
43		sseq1 2072	. . . . . . . . . . . . . . . 16 ⊢ (y = z → (y ⊆ x ↔ z ⊆ x))
44	43	cbvrexv 1792	. . . . . . . . . . . . . . 15 ⊢ (∃y ∈ (fi ‘A)y ⊆ x ↔ ∃z ∈ (fi ‘A)z ⊆ x)
45	42, 44	syl5bb 530	. . . . . . . . . . . . . 14 ⊢ (x = y → (∃y ∈ (fi ‘A)y ⊆ x ↔ ∃z ∈ (fi ‘A)z ⊆ y))
46	45	elrab 1896	. . . . . . . . . . . . 13 ⊢ (y ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ↔ (y ∈ ℘X ⋀ ∃z ∈ (fi ‘A)z ⊆ y))
47	40, 46	sylibr 200	. . . . . . . . . . . 12 ⊢ (((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) ⋀ y ∈ (fi ‘A)) → y ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x})
48	47, 35	jctil 292	. . . . . . . . . . 11 ⊢ (((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) ⋀ y ∈ (fi ‘A)) → (y ⊆ y ⋀ y ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x}))
49		ssuni 2512	. . . . . . . . . . 11 ⊢ ((y ⊆ y ⋀ y ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x}) → y ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x})
50	48, 49	syl 10	. . . . . . . . . 10 ⊢ (((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) ⋀ y ∈ (fi ‘A)) → y ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x})
51	50	r19.21aiva 1706	. . . . . . . . 9 ⊢ ((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) → ∀y ∈ (fi ‘A)y ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x})
52	14, 22, 51	sylanc 471	. . . . . . . 8 ⊢ ((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) → ∃y ∈ (fi ‘A)y ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x})
53	13, 52	jca 288	. . . . . . 7 ⊢ ((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) → (∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ∈ ℘X ⋀ ∃y ∈ (fi ‘A)y ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x}))
54	53	adantr 389	. . . . . 6 ⊢ (((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) ⋀ ¬ ∅ ∈ (fi ‘A)) → (∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ∈ ℘X ⋀ ∃y ∈ (fi ‘A)y ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x}))
55		hbrab1 1764	. . . . . . . 8 ⊢ (z ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} → ∀x z ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x})
56	55	hbuni 2499	. . . . . . 7 ⊢ (z ∈ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} → ∀x z ∈ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x})
57		ax-17 968	. . . . . . . 8 ⊢ (z ∈ X → ∀x z ∈ X)
58	57	hbpw 2397	. . . . . . 7 ⊢ (z ∈ ℘X → ∀x z ∈ ℘X)
59		ax-17 968	. . . . . . . 8 ⊢ (y ∈ (fi ‘A) → ∀x y ∈ (fi ‘A))
60		ax-17 968	. . . . . . . . 9 ⊢ (z ∈ y → ∀x z ∈ y)
61	60, 56	hbss 2052	. . . . . . . 8 ⊢ (y ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} → ∀x y ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x})
62	59, 61	hbrex 1680	. . . . . . 7 ⊢ (∃y ∈ (fi ‘A)y ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} → ∀x∃y ∈ (fi ‘A)y ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x})
63		ax-17 968	. . . . . . . . 9 ⊢ (w ∈ x → ∀y w ∈ x)
64		hbre1 1681	. . . . . . . . . . 11 ⊢ (∃y ∈ (fi ‘A)y ⊆ x → ∀y∃y ∈ (fi ‘A)y ⊆ x)
65		ax-17 968	. . . . . . . . . . 11 ⊢ (z ∈ ℘X → ∀y z ∈ ℘X)
66	64, 65	hbrab 1765	. . . . . . . . . 10 ⊢ (z ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} → ∀y z ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x})
67	66	hbuni 2499	. . . . . . . . 9 ⊢ (z ∈ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} → ∀y z ∈ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x})
68	63, 67	hbeq 1557	. . . . . . . 8 ⊢ (x = ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} → ∀y x = ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x})
69		sseq2 2073	. . . . . . . 8 ⊢ (x = ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} → (y ⊆ x ↔ y ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x}))
70	68, 69	rexbid 1654	. . . . . . 7 ⊢ (x = ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} → (∃y ∈ (fi ‘A)y ⊆ x ↔ ∃y ∈ (fi ‘A)y ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x}))
71	56, 58, 62, 70	elrabf 1895	. . . . . 6 ⊢ (∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ↔ (∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ∈ ℘X ⋀ ∃y ∈ (fi ‘A)y ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x}))
72	54, 71	sylibr 200	. . . . 5 ⊢ (((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) ⋀ ¬ ∅ ∈ (fi ‘A)) → ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x})
73	11, 72	jca 288	. . . 4 ⊢ (((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) ⋀ ¬ ∅ ∈ (fi ‘A)) → (¬ ∅ ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ⋀ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x}))
74		visset 1804	. . . . . . . . . . . 12 ⊢ b ∈ V
75	74	elpw 2394	. . . . . . . . . . 11 ⊢ (b ∈ ℘∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ↔ b ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x})
76		unissb 2518	. . . . . . . . . . . . . 14 ⊢ (∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ⊆ X ↔ ∀t ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x}t ⊆ X)
77		sseq2 2073	. . . . . . . . . . . . . . . . 17 ⊢ (x = t → (y ⊆ x ↔ y ⊆ t))
78	77	rexbidv 1656	. . . . . . . . . . . . . . . 16 ⊢ (x = t → (∃y ∈ (fi ‘A)y ⊆ x ↔ ∃y ∈ (fi ‘A)y ⊆ t))
79	78	elrab 1896	. . . . . . . . . . . . . . 15 ⊢ (t ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ↔ (t ∈ ℘X ⋀ ∃y ∈ (fi ‘A)y ⊆ t))
80		elpwi 2396	. . . . . . . . . . . . . . . 16 ⊢ (t ∈ ℘X → t ⊆ X)
81	80	adantr 389	. . . . . . . . . . . . . . 15 ⊢ ((t ∈ ℘X ⋀ ∃y ∈ (fi ‘A)y ⊆ t) → t ⊆ X)
82	79, 81	sylbi 199	. . . . . . . . . . . . . 14 ⊢ (t ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} → t ⊆ X)
83	76, 82	mprgbir 1693	. . . . . . . . . . . . 13 ⊢ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ⊆ X
84		sspwb 2745	. . . . . . . . . . . . 13 ⊢ (∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ⊆ X ↔ ℘∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ⊆ ℘X)
85	83, 84	mpbi 189	. . . . . . . . . . . 12 ⊢ ℘∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ⊆ ℘X
86	85	sseli 2055	. . . . . . . . . . 11 ⊢ (b ∈ ℘∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} → b ∈ ℘X)
87	75, 86	sylbir 201	. . . . . . . . . 10 ⊢ (b ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} → b ∈ ℘X)
88	87	3ad2ant2 799	. . . . . . . . 9 ⊢ (((a ∈ ℘X ⋀ ∃y ∈ (fi ‘A)y ⊆ a) ⋀ b ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ⋀ a ⊆ b) → b ∈ ℘X)
89		r19.41v 1755	. . . . . . . . . . . 12 ⊢ (∃y ∈ (fi ‘A)(y ⊆ a ⋀ a ⊆ b) ↔ (∃y ∈ (fi ‘A)y ⊆ a ⋀ a ⊆ b))
90		sstr 2062	. . . . . . . . . . . . 13 ⊢ ((y ⊆ a ⋀ a ⊆ b) → y ⊆ b)
91	90	r19.22si 1726	. . . . . . . . . . . 12 ⊢ (∃y ∈ (fi ‘A)(y ⊆ a ⋀ a ⊆ b) → ∃y ∈ (fi ‘A)y ⊆ b)
92	89, 91	sylbir 201	. . . . . . . . . . 11 ⊢ ((∃y ∈ (fi ‘A)y ⊆ a ⋀ a ⊆ b) → ∃y ∈ (fi ‘A)y ⊆ b)
93	92	adantll 392	. . . . . . . . . 10 ⊢ (((a ∈ ℘X ⋀ ∃y ∈ (fi ‘A)y ⊆ a) ⋀ a ⊆ b) → ∃y ∈ (fi ‘A)y ⊆ b)
94	93	3adant2 796	. . . . . . . . 9 ⊢ (((a ∈ ℘X ⋀ ∃y ∈ (fi ‘A)y ⊆ a) ⋀ b ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ⋀ a ⊆ b) → ∃y ∈ (fi ‘A)y ⊆ b)
95	88, 94	jca 288	. . . . . . . 8 ⊢ (((a ∈ ℘X ⋀ ∃y ∈ (fi ‘A)y ⊆ a) ⋀ b ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ⋀ a ⊆ b) → (b ∈ ℘X ⋀ ∃y ∈ (fi ‘A)y ⊆ b))
96		sseq2 2073	. . . . . . . . . 10 ⊢ (x = a → (y ⊆ x ↔ y ⊆ a))
97	96	rexbidv 1656	. . . . . . . . 9 ⊢ (x = a → (∃y ∈ (fi ‘A)y ⊆ x ↔ ∃y ∈ (fi ‘A)y ⊆ a))
98	97	elrab 1896	. . . . . . . 8 ⊢ (a ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ↔ (a ∈ ℘X ⋀ ∃y ∈ (fi ‘A)y ⊆ a))
99	95, 98	syl3an1b 860	. . . . . . 7 ⊢ ((a ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ⋀ b ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ⋀ a ⊆ b) → (b ∈ ℘X ⋀ ∃y ∈ (fi ‘A)y ⊆ b))
100		sseq2 2073	. . . . . . . . 9 ⊢ (x = b → (y ⊆ x ↔ y ⊆ b))
101	100	rexbidv 1656	. . . . . . . 8 ⊢ (x = b → (∃y ∈ (fi ‘A)y ⊆ x ↔ ∃y ∈ (fi ‘A)y ⊆ b))
102	101	elrab 1896	. . . . . . 7 ⊢ (b ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ↔ (b ∈ ℘X ⋀ ∃y ∈ (fi ‘A)y ⊆ b))
103	99, 102	sylibr 200	. . . . . 6 ⊢ ((a ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ⋀ b ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ⋀ a ⊆ b) → b ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x})
104	103	gen2 980	. . . . 5 ⊢ ∀a∀b((a ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ⋀ b ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ⋀ a ⊆ b) → b ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x})
105	104	a1i 8	. . . 4 ⊢ (((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) ⋀ ¬ ∅ ∈ (fi ‘A)) → ∀a∀b((a ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ⋀ b ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ⋀ a ⊆ b) → b ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x}))
106		inpws1 10351	. . . . . . . . . . 11 ⊢ (a ∈ ℘X → (a ∩ b) ∈ ℘X)
107	106	adantr 389	. . . . . . . . . 10 ⊢ ((a ∈ ℘X ⋀ b ∈ ℘X) → (a ∩ b) ∈ ℘X)
108		ax-17 968	. . . . . . . . . . . . . . . . . . 19 ⊢ ((u ∩ v) ⊆ (a ∩ b) → ∀y(u ∩ v) ⊆ (a ∩ b))
109		sseq1 2072	. . . . . . . . . . . . . . . . . . 19 ⊢ (y = (u ∩ v) → (y ⊆ (a ∩ b) ↔ (u ∩ v) ⊆ (a ∩ b)))
110	108, 109	rcla4e 1863	. . . . . . . . . . . . . . . . . 18 ⊢ (((u ∩ v) ∈ (fi ‘A) ⋀ (u ∩ v) ⊆ (a ∩ b)) → ∃y ∈ (fi ‘A)y ⊆ (a ∩ b))
111		elfvdm 3732	. . . . . . . . . . . . . . . . . . . 20 ⊢ (u ∈ (fi ‘A) → A ∈ dom fi)
112		infi 10448	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (A ∈ dom fi → ((u ∈ (fi ‘A) ⋀ v ∈ (fi ‘A)) → (u ∩ v) ∈ (fi ‘A)))
113	112	exp3a 375	. . . . . . . . . . . . . . . . . . . 20 ⊢ (A ∈ dom fi → (u ∈ (fi ‘A) → (v ∈ (fi ‘A) → (u ∩ v) ∈ (fi ‘A))))
114	111, 113	mpcom 49	. . . . . . . . . . . . . . . . . . 19 ⊢ (u ∈ (fi ‘A) → (v ∈ (fi ‘A) → (u ∩ v) ∈ (fi ‘A)))
115	114	imp 350	. . . . . . . . . . . . . . . . . 18 ⊢ ((u ∈ (fi ‘A) ⋀ v ∈ (fi ‘A)) → (u ∩ v) ∈ (fi ‘A))
116		ss2in 2226	. . . . . . . . . . . . . . . . . 18 ⊢ ((u ⊆ a ⋀ v ⊆ b) → (u ∩ v) ⊆ (a ∩ b))
117	110, 115, 116	syl2an 454	. . . . . . . . . . . . . . . . 17 ⊢ (((u ∈ (fi ‘A) ⋀ v ∈ (fi ‘A)) ⋀ (u ⊆ a ⋀ v ⊆ b)) → ∃y ∈ (fi ‘A)y ⊆ (a ∩ b))
118	117	an4s 507	. . . . . . . . . . . . . . . 16 ⊢ (((u ∈ (fi ‘A) ⋀ u ⊆ a) ⋀ (v ∈ (fi ‘A) ⋀ v ⊆ b)) → ∃y ∈ (fi ‘A)y ⊆ (a ∩ b))
119	118	expcom 374	. . . . . . . . . . . . . . 15 ⊢ ((v ∈ (fi ‘A) ⋀ v ⊆ b) → ((u ∈ (fi ‘A) ⋀ u ⊆ a) → ∃y ∈ (fi ‘A)y ⊆ (a ∩ b)))
120	119	r19.23aiva 1736	. . . . . . . . . . . . . 14 ⊢ (∃v ∈ (fi ‘A)v ⊆ b → ((u ∈ (fi ‘A) ⋀ u ⊆ a) → ∃y ∈ (fi ‘A)y ⊆ (a ∩ b)))
121	120	com12 11	. . . . . . . . . . . . 13 ⊢ ((u ∈ (fi ‘A) ⋀ u ⊆ a) → (∃v ∈ (fi ‘A)v ⊆ b → ∃y ∈ (fi ‘A)y ⊆ (a ∩ b)))
122	121	r19.23aiva 1736	. . . . . . . . . . . 12 ⊢ (∃u ∈ (fi ‘A)u ⊆ a → (∃v ∈ (fi ‘A)v ⊆ b → ∃y ∈ (fi ‘A)y ⊆ (a ∩ b)))
123	122	imp 350	. . . . . . . . . . 11 ⊢ ((∃u ∈ (fi ‘A)u ⊆ a ⋀ ∃v ∈ (fi ‘A)v ⊆ b) → ∃y ∈ (fi ‘A)y ⊆ (a ∩ b))
124		sseq1 2072	. . . . . . . . . . . 12 ⊢ (y = u → (y ⊆ a ↔ u ⊆ a))
125	124	cbvrexv 1792	. . . . . . . . . . 11 ⊢ (∃y ∈ (fi ‘A)y ⊆ a ↔ ∃u ∈ (fi ‘A)u ⊆ a)
126		sseq1 2072	. . . . . . . . . . . 12 ⊢ (y = v → (y ⊆ b ↔ v ⊆ b))
127	126	cbvrexv 1792	. . . . . . . . . . 11 ⊢ (∃y ∈ (fi ‘A)y ⊆ b ↔ ∃v ∈ (fi ‘A)v ⊆ b)
128	123, 125, 127	syl2anb 455	. . . . . . . . . 10 ⊢ ((∃y ∈ (fi ‘A)y ⊆ a ⋀ ∃y ∈ (fi ‘A)y ⊆ b) → ∃y ∈ (fi ‘A)y ⊆ (a ∩ b))
129	107, 128	anim12i 333	. . . . . . . . 9 ⊢ (((a ∈ ℘X ⋀ b ∈ ℘X) ⋀ (∃y ∈ (fi ‘A)y ⊆ a ⋀ ∃y ∈ (fi ‘A)y ⊆ b)) → ((a ∩ b) ∈ ℘X ⋀ ∃y ∈ (fi ‘A)y ⊆ (a ∩ b)))
130	129	an4s 507	. . . . . . . 8 ⊢ (((a ∈ ℘X ⋀ ∃y ∈ (fi ‘A)y ⊆ a) ⋀ (b ∈ ℘X ⋀ ∃y ∈ (fi ‘A)y ⊆ b)) → ((a ∩ b) ∈ ℘X ⋀ ∃y ∈ (fi ‘A)y ⊆ (a ∩ b)))
131		pm3.26 319	. . . . . . . . . . 11 ⊢ ((x = (a ∩ b) ⋀ y ∈ (fi ‘A)) → x = (a ∩ b))
132	131	sseq2d 2079	. . . . . . . . . 10 ⊢ ((x = (a ∩ b) ⋀ y ∈ (fi ‘A)) → (y ⊆ x ↔ y ⊆ (a ∩ b)))
133	132	rexbidva 1652	. . . . . . . . 9 ⊢ (x = (a ∩ b) → (∃y ∈ (fi ‘A)y ⊆ x ↔ ∃y ∈ (fi ‘A)y ⊆ (a ∩ b)))
134	133	elrab 1896	. . . . . . . 8 ⊢ ((a ∩ b) ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ↔ ((a ∩ b) ∈ ℘X ⋀ ∃y ∈ (fi ‘A)y ⊆ (a ∩ b)))
135	130, 134	sylibr 200	. . . . . . 7 ⊢ (((a ∈ ℘X ⋀ ∃y ∈ (fi ‘A)y ⊆ a) ⋀ (b ∈ ℘X ⋀ ∃y ∈ (fi ‘A)y ⊆ b)) → (a ∩ b) ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x})
136		pm3.26 319	. . . . . . . . . 10 ⊢ ((x = a ⋀ y ∈ (fi ‘A)) → x = a)
137	136	sseq2d 2079	. . . . . . . . 9 ⊢ ((x = a ⋀ y ∈ (fi ‘A)) → (y ⊆ x ↔ y ⊆ a))
138	137	rexbidva 1652	. . . . . . . 8 ⊢ (x = a → (∃y ∈ (fi ‘A)y ⊆ x ↔ ∃y ∈ (fi ‘A)y ⊆ a))
139	138	elrab 1896	. . . . . . 7 ⊢ (a ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ↔ (a ∈ ℘X ⋀ ∃y ∈ (fi ‘A)y ⊆ a))
140		pm3.26 319	. . . . . . . . . 10 ⊢ ((x = b ⋀ y ∈ (fi ‘A)) → x = b)
141	140	sseq2d 2079	. . . . . . . . 9 ⊢ ((x = b ⋀ y ∈ (fi ‘A)) → (y ⊆ x ↔ y ⊆ b))
142	141	rexbidva 1652	. . . . . . . 8 ⊢ (x = b → (∃y ∈ (fi ‘A)y ⊆ x ↔ ∃y ∈ (fi ‘A)y ⊆ b))
143	142	elrab 1896	. . . . . . 7 ⊢ (b ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ↔ (b ∈ ℘X ⋀ ∃y ∈ (fi ‘A)y ⊆ b))
144	135, 139, 143	syl2anb 455	. . . . . 6 ⊢ ((a ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ⋀ b ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x}) → (a ∩ b) ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x})
145	144	rgen2 1715	. . . . 5 ⊢ ∀a ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x}∀b ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} (a ∩ b) ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x}
146	145	a1i 8	. . . 4 ⊢ (((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) ⋀ ¬ ∅ ∈ (fi ‘A)) → ∀a ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x}∀b ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} (a ∩ b) ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x})
147	73, 105, 146	3jca 817	. . 3 ⊢ (((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) ⋀ ¬ ∅ ∈ (fi ‘A)) → ((¬ ∅ ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ⋀ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x}) ⋀ ∀a∀b((a ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ⋀ b ⊆ ∪{x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ⋀ a ⊆ b) → b ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x}) ⋀ ∀a ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x}∀b ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} (a ∩ b) ∈ {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x}))
148		rabexg 2714	. . . . . . 7 ⊢ (℘X ∈ V → {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ∈ V)
149	18, 148	syl 10	. . . . . 6 ⊢ (X ∈ V → {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ∈ V)
150	149	3ad2ant2 799	. . . . 5 ⊢ ((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) → {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ∈ V)
151	150	adantr 389	. . . 4 ⊢ (((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) ⋀ ¬ ∅ ∈ (fi ‘A)) → {x ∈ ℘X∣∃