Theorem alexsubALT 22226

Description: The Alexander Subbase Theorem: a space is compact iff it has a subbase such that any cover taken from the subbase has a finite subcover. (Contributed by Jeff Hankins, 24-Jan-2010.) (Revised by Mario Carneiro, 11-Feb-2015.) (New usage is discouraged.) (Proof modification is discouraged.)

Hypothesis

Ref	Expression
alexsubALT.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
alexsubALT	⊢ (𝐽 ∈ Comp ↔ ∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))

Distinct variable groups:   𝑐,𝑑,𝑥,𝐽   𝑋,𝑐,𝑑,𝑥

Proof of Theorem alexsubALT

Dummy variables 𝑎 𝑏 𝑓 𝑡 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		alexsubALT.1	. . 3 ⊢ 𝑋 = ∪ 𝐽
2	1	alexsubALTlem1 22222	. 2 ⊢ (𝐽 ∈ Comp → ∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
3	1	alexsubALTlem4 22225	. . . . 5 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → ∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
4		selpw 4386	. . . . . . . . 9 ⊢ (𝑐 ∈ 𝒫 𝐽 ↔ 𝑐 ⊆ 𝐽)
5		eleq2 2896	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋 = ∪ 𝑐 → (𝑡 ∈ 𝑋 ↔ 𝑡 ∈ ∪ 𝑐))
6	5	3ad2ant3 1171	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑋 ↔ 𝑡 ∈ ∪ 𝑐))
7		eluni 4662	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ ∪ 𝑐 ↔ ∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑐))
8		ssel 3822	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑐 ⊆ 𝐽 → (𝑤 ∈ 𝑐 → 𝑤 ∈ 𝐽))
9		eleq2 2896	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (𝑤 ∈ 𝐽 ↔ 𝑤 ∈ (topGen‘(fi‘𝑥))))
10		tg2 21141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑤 ∈ (topGen‘(fi‘𝑥)) ∧ 𝑡 ∈ 𝑤) → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤))
11	10	ex 403	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 ∈ (topGen‘(fi‘𝑥)) → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤)))
12	9, 11	syl6bi 245	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (𝑤 ∈ 𝐽 → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤))))
13	8, 12	sylan9r 506	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → (𝑤 ∈ 𝑐 → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤))))
14	13	3impia 1151	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤)))
15		sseq2 3853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = 𝑤 → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑤))
16	15	rspcev 3527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑤 ∈ 𝑐 ∧ 𝑦 ⊆ 𝑤) → ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)
17	16	ex 403	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 ∈ 𝑐 → (𝑦 ⊆ 𝑤 → ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))
18	17	3ad2ant3 1171	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → (𝑦 ⊆ 𝑤 → ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))
19	18	anim2d 607	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → ((𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤) → (𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
20	19	reximdv 3225	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → (∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤) → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
21	14, 20	syld 47	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
22	21	3expia 1156	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → (𝑤 ∈ 𝑐 → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))))
23	22	com23 86	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → (𝑡 ∈ 𝑤 → (𝑤 ∈ 𝑐 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))))
24	23	impd 400	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → ((𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑐) → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
25	24	exlimdv 2034	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → (∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑐) → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
26	7, 25	syl5bi 234	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → (𝑡 ∈ ∪ 𝑐 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
27	26	3adant3 1168	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ ∪ 𝑐 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
28	6, 27	sylbid 232	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑋 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
29		ssel 3822	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ⊆ 𝑧 → (𝑡 ∈ 𝑦 → 𝑡 ∈ 𝑧))
30		elunii 4664	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ 𝑧 ∧ 𝑧 ∈ 𝑐) → 𝑡 ∈ ∪ 𝑐)
31	30	expcom 404	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ 𝑐 → (𝑡 ∈ 𝑧 → 𝑡 ∈ ∪ 𝑐))
32	6	biimprd 240	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ ∪ 𝑐 → 𝑡 ∈ 𝑋))
33	31, 32	sylan9r 506	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑧 ∈ 𝑐) → (𝑡 ∈ 𝑧 → 𝑡 ∈ 𝑋))
34	29, 33	syl9r 78	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑧 ∈ 𝑐) → (𝑦 ⊆ 𝑧 → (𝑡 ∈ 𝑦 → 𝑡 ∈ 𝑋)))
35	34	rexlimdva 3241	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 → (𝑡 ∈ 𝑦 → 𝑡 ∈ 𝑋)))
36	35	com23 86	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑦 → (∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 → 𝑡 ∈ 𝑋)))
37	36	impd 400	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → ((𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧) → 𝑡 ∈ 𝑋))
38	37	rexlimdvw 3245	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧) → 𝑡 ∈ 𝑋))
39	28, 38	impbid 204	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑋 ↔ ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
40		elunirab 4671	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ↔ ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))
41	39, 40	syl6bbr 281	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑋 ↔ 𝑡 ∈ ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧}))
42	41	eqrdv 2824	. . . . . . . . . . . . . 14 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → 𝑋 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧})
43		ssrab2 3913	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ⊆ (fi‘𝑥)
44		fvex 6447	. . . . . . . . . . . . . . . . 17 ⊢ (fi‘𝑥) ∈ V
45	44	elpw2 5051	. . . . . . . . . . . . . . . 16 ⊢ ({𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∈ 𝒫 (fi‘𝑥) ↔ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ⊆ (fi‘𝑥))
46	43, 45	mpbir 223	. . . . . . . . . . . . . . 15 ⊢ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∈ 𝒫 (fi‘𝑥)
47		unieq 4667	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∪ 𝑎 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧})
48	47	eqeq2d 2836	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑋 = ∪ 𝑎 ↔ 𝑋 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧}))
49		pweq 4382	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → 𝒫 𝑎 = 𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧})
50	49	ineq1d 4041	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝒫 𝑎 ∩ Fin) = (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin))
51	50	rexeqdv 3358	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏 ↔ ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)𝑋 = ∪ 𝑏))
52	48, 51	imbi12d 336	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ((𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) ↔ (𝑋 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)𝑋 = ∪ 𝑏)))
53	52	rspcv 3523	. . . . . . . . . . . . . . 15 ⊢ ({𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∈ 𝒫 (fi‘𝑥) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → (𝑋 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)𝑋 = ∪ 𝑏)))
54	46, 53	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → (𝑋 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)𝑋 = ∪ 𝑏))
55	42, 54	syl5com 31	. . . . . . . . . . . . 13 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)𝑋 = ∪ 𝑏))
56		elfpw 8538	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin) ↔ (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∧ 𝑏 ∈ Fin))
57		ssel 3822	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑡 ∈ 𝑏 → 𝑡 ∈ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧}))
58		sseq1 3852	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑡 → (𝑦 ⊆ 𝑧 ↔ 𝑡 ⊆ 𝑧))
59	58	rexbidv 3263	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑡 → (∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 ↔ ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧))
60	59	elrab 3586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 ∈ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ↔ (𝑡 ∈ (fi‘𝑥) ∧ ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧))
61	60	simprbi 492	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧)
62	57, 61	syl6 35	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑡 ∈ 𝑏 → ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧))
63	62	ralrimiv 3175	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∀𝑡 ∈ 𝑏 ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧)
64		sseq2 3853	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = (𝑓‘𝑡) → (𝑡 ⊆ 𝑧 ↔ 𝑡 ⊆ (𝑓‘𝑡)))
65	64	ac6sfi 8474	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑏 ∈ Fin ∧ ∀𝑡 ∈ 𝑏 ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧) → ∃𝑓(𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)))
66	65	ex 403	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ Fin → (∀𝑡 ∈ 𝑏 ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧 → ∃𝑓(𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡))))
67	63, 66	syl5 34	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ Fin → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∃𝑓(𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡))))
68	67	adantl 475	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∃𝑓(𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡))))
69		simprll 799	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑓:𝑏⟶𝑐)
70		frn 6285	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓:𝑏⟶𝑐 → ran 𝑓 ⊆ 𝑐)
71	69, 70	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ran 𝑓 ⊆ 𝑐)
72		simplr 787	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑏 ∈ Fin)
73		ffn 6279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓:𝑏⟶𝑐 → 𝑓 Fn 𝑏)
74		dffn4 6360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 Fn 𝑏 ↔ 𝑓:𝑏–onto→ran 𝑓)
75	73, 74	sylib 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:𝑏⟶𝑐 → 𝑓:𝑏–onto→ran 𝑓)
76	75	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) → 𝑓:𝑏–onto→ran 𝑓)
77	76	ad2antrl 721	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑓:𝑏–onto→ran 𝑓)
78		fodomfi 8509	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑏 ∈ Fin ∧ 𝑓:𝑏–onto→ran 𝑓) → ran 𝑓 ≼ 𝑏)
79	72, 77, 78	syl2anc 581	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ran 𝑓 ≼ 𝑏)
80		domfi 8451	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 ∈ Fin ∧ ran 𝑓 ≼ 𝑏) → ran 𝑓 ∈ Fin)
81	72, 79, 80	syl2anc 581	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ran 𝑓 ∈ Fin)
82	71, 81	jca 509	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → (ran 𝑓 ⊆ 𝑐 ∧ ran 𝑓 ∈ Fin))
83		elin 4024	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ↔ (ran 𝑓 ∈ 𝒫 𝑐 ∧ ran 𝑓 ∈ Fin))
84		vex 3418	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑐 ∈ V
85	84	elpw2 5051	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ran 𝑓 ∈ 𝒫 𝑐 ↔ ran 𝑓 ⊆ 𝑐)
86	85	anbi1i 619	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ran 𝑓 ∈ 𝒫 𝑐 ∧ ran 𝑓 ∈ Fin) ↔ (ran 𝑓 ⊆ 𝑐 ∧ ran 𝑓 ∈ Fin))
87	83, 86	bitr2i 268	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ran 𝑓 ⊆ 𝑐 ∧ ran 𝑓 ∈ Fin) ↔ ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin))
88	82, 87	sylib 210	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin))
89		simprr 791	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑋 = ∪ 𝑏)
90		uniiun 4794	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ∪ 𝑏 = ∪ 𝑡 ∈ 𝑏 𝑡
91		simprlr 800	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡))
92		ss2iun 4757	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡) → ∪ 𝑡 ∈ 𝑏 𝑡 ⊆ ∪ 𝑡 ∈ 𝑏 (𝑓‘𝑡))
93	91, 92	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ 𝑡 ∈ 𝑏 𝑡 ⊆ ∪ 𝑡 ∈ 𝑏 (𝑓‘𝑡))
94	90, 93	syl5eqss 3875	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ 𝑏 ⊆ ∪ 𝑡 ∈ 𝑏 (𝑓‘𝑡))
95		fniunfv 6761	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 Fn 𝑏 → ∪ 𝑡 ∈ 𝑏 (𝑓‘𝑡) = ∪ ran 𝑓)
96	69, 73, 95	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ 𝑡 ∈ 𝑏 (𝑓‘𝑡) = ∪ ran 𝑓)
97	94, 96	sseqtrd 3867	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ 𝑏 ⊆ ∪ ran 𝑓)
98	89, 97	eqsstrd 3865	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑋 ⊆ ∪ ran 𝑓)
99		simpll2 1277	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑐 ⊆ 𝐽)
100	71, 99	sstrd 3838	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ran 𝑓 ⊆ 𝐽)
101		uniss 4682	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ran 𝑓 ⊆ 𝐽 → ∪ ran 𝑓 ⊆ ∪ 𝐽)
102	101, 1	syl6sseqr 3878	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ran 𝑓 ⊆ 𝐽 → ∪ ran 𝑓 ⊆ 𝑋)
103	100, 102	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ ran 𝑓 ⊆ 𝑋)
104	98, 103	eqssd 3845	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑋 = ∪ ran 𝑓)
105		unieq 4667	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = ran 𝑓 → ∪ 𝑑 = ∪ ran 𝑓)
106	105	eqeq2d 2836	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = ran 𝑓 → (𝑋 = ∪ 𝑑 ↔ 𝑋 = ∪ ran 𝑓))
107	106	rspcev 3527	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑋 = ∪ ran 𝑓) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)
108	88, 104, 107	syl2anc 581	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)
109	108	exp32 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) → ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
110	109	exlimdv 2034	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) → (∃𝑓(𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
111	68, 110	syld 47	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
112	111	ex 403	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑏 ∈ Fin → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))))
113	112	com23 86	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑏 ∈ Fin → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))))
114	113	impd 400	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → ((𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∧ 𝑏 ∈ Fin) → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
115	56, 114	syl5bi 234	. . . . . . . . . . . . . 14 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin) → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
116	115	rexlimdv 3240	. . . . . . . . . . . . 13 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))
117	55, 116	syld 47	. . . . . . . . . . . 12 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))
118	117	3exp 1154	. . . . . . . . . . 11 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (𝑐 ⊆ 𝐽 → (𝑋 = ∪ 𝑐 → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))))
119	118	com34 91	. . . . . . . . . 10 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (𝑐 ⊆ 𝐽 → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → (𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))))
120	119	com23 86	. . . . . . . . 9 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → (𝑐 ⊆ 𝐽 → (𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))))
121	4, 120	syl7bi 247	. . . . . . . 8 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → (𝑐 ∈ 𝒫 𝐽 → (𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))))
122	121	ralrimdv 3178	. . . . . . 7 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
123		fibas 21153	. . . . . . . . 9 ⊢ (fi‘𝑥) ∈ TopBases
124		tgcl 21145	. . . . . . . . 9 ⊢ ((fi‘𝑥) ∈ TopBases → (topGen‘(fi‘𝑥)) ∈ Top)
125	123, 124	ax-mp 5	. . . . . . . 8 ⊢ (topGen‘(fi‘𝑥)) ∈ Top
126		eleq1 2895	. . . . . . . 8 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (𝐽 ∈ Top ↔ (topGen‘(fi‘𝑥)) ∈ Top))
127	125, 126	mpbiri 250	. . . . . . 7 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → 𝐽 ∈ Top)
128	122, 127	jctild 523	. . . . . 6 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → (𝐽 ∈ Top ∧ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))))
129	1	iscmp 21563	. . . . . 6 ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
130	128, 129	syl6ibr 244	. . . . 5 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → 𝐽 ∈ Comp))
131	3, 130	syld 47	. . . 4 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → 𝐽 ∈ Comp))
132	131	imp 397	. . 3 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)) → 𝐽 ∈ Comp)
133	132	exlimiv 2031	. 2 ⊢ (∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)) → 𝐽 ∈ Comp)
134	2, 133	impbii 201	1 ⊢ (𝐽 ∈ Comp ↔ ∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   ∧ w3a 1113   = wceq 1658  ∃wex 1880   ∈ wcel 2166  ∀wral 3118  ∃wrex 3119  {crab 3122   ∩ cin 3798   ⊆ wss 3799  𝒫 cpw 4379  ∪ cuni 4659  ∪ ciun 4741   class class class wbr 4874  ran crn 5344   Fn wfn 6119  ⟶wf 6120  –onto→wfo 6122  ‘cfv 6124   ≼ cdom 8221  Fincfn 8223  ficfi 8586  topGenctg 16452  Topctop 21069  TopBasesctb 21121  Compccmp 21561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-rep 4995  ax-sep 5006  ax-nul 5014  ax-pow 5066  ax-pr 5128  ax-un 7210  ax-ac2 9601

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ne 3001  df-ral 3123  df-rex 3124  df-reu 3125  df-rmo 3126  df-rab 3127  df-v 3417  df-sbc 3664  df-csb 3759  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-pss 3815  df-nul 4146  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4660  df-int 4699  df-iun 4743  df-br 4875  df-opab 4937  df-mpt 4954  df-tr 4977  df-id 5251  df-eprel 5256  df-po 5264  df-so 5265  df-fr 5302  df-se 5303  df-we 5304  df-xp 5349  df-rel 5350  df-cnv 5351  df-co 5352  df-dm 5353  df-rn 5354  df-res 5355  df-ima 5356  df-pred 5921  df-ord 5967  df-on 5968  df-lim 5969  df-suc 5970  df-iota 6087  df-fun 6126  df-fn 6127  df-f 6128  df-f1 6129  df-fo 6130  df-f1o 6131  df-fv 6132  df-isom 6133  df-riota 6867  df-ov 6909  df-oprab 6910  df-mpt2 6911  df-rpss 7198  df-om 7328  df-wrecs 7673  df-recs 7735  df-rdg 7773  df-1o 7827  df-oadd 7831  df-er 8010  df-en 8224  df-dom 8225  df-fin 8227  df-fi 8587  df-card 9079  df-ac 9253  df-topgen 16458  df-top 21070  df-bases 21122  df-cmp 21562

This theorem is referenced by: (None)