Theorem alexsubALT 23945

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 23941	. 2 ⊢ (𝐽 ∈ Comp → ∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
3	1	alexsubALTlem4 23944	. . . . 5 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → ∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
4		velpw 4571	. . . . . . . . 9 ⊢ (𝑐 ∈ 𝒫 𝐽 ↔ 𝑐 ⊆ 𝐽)
5		eleq2 2818	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋 = ∪ 𝑐 → (𝑡 ∈ 𝑋 ↔ 𝑡 ∈ ∪ 𝑐))
6	5	3ad2ant3 1135	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑋 ↔ 𝑡 ∈ ∪ 𝑐))
7		eluni 4877	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ ∪ 𝑐 ↔ ∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑐))
8		ssel 3943	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑐 ⊆ 𝐽 → (𝑤 ∈ 𝑐 → 𝑤 ∈ 𝐽))
9		eleq2 2818	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (𝑤 ∈ 𝐽 ↔ 𝑤 ∈ (topGen‘(fi‘𝑥))))
10		tg2 22859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑤 ∈ (topGen‘(fi‘𝑥)) ∧ 𝑡 ∈ 𝑤) → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤))
11	10	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 ∈ (topGen‘(fi‘𝑥)) → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤)))
12	9, 11	biimtrdi 253	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (𝑤 ∈ 𝐽 → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤))))
13	8, 12	sylan9r 508	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → (𝑤 ∈ 𝑐 → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤))))
14	13	3impia 1117	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤)))
15		sseq2 3976	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = 𝑤 → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑤))
16	15	rspcev 3591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑤 ∈ 𝑐 ∧ 𝑦 ⊆ 𝑤) → ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)
17	16	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 ∈ 𝑐 → (𝑦 ⊆ 𝑤 → ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))
18	17	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → (𝑦 ⊆ 𝑤 → ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))
19	18	anim2d 612	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → ((𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤) → (𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
20	19	reximdv 3149	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → (∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤) → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
21	14, 20	syld 47	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
22	21	3expia 1121	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → (𝑤 ∈ 𝑐 → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))))
23	22	com23 86	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → (𝑡 ∈ 𝑤 → (𝑤 ∈ 𝑐 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))))
24	23	impd 410	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → ((𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑐) → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
25	24	exlimdv 1933	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → (∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑐) → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
26	7, 25	biimtrid 242	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → (𝑡 ∈ ∪ 𝑐 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
27	26	3adant3 1132	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ ∪ 𝑐 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
28	6, 27	sylbid 240	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑋 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
29		ssel 3943	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ⊆ 𝑧 → (𝑡 ∈ 𝑦 → 𝑡 ∈ 𝑧))
30		elunii 4879	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ 𝑧 ∧ 𝑧 ∈ 𝑐) → 𝑡 ∈ ∪ 𝑐)
31	30	expcom 413	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ 𝑐 → (𝑡 ∈ 𝑧 → 𝑡 ∈ ∪ 𝑐))
32	6	biimprd 248	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ ∪ 𝑐 → 𝑡 ∈ 𝑋))
33	31, 32	sylan9r 508	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑧 ∈ 𝑐) → (𝑡 ∈ 𝑧 → 𝑡 ∈ 𝑋))
34	29, 33	syl9r 78	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑧 ∈ 𝑐) → (𝑦 ⊆ 𝑧 → (𝑡 ∈ 𝑦 → 𝑡 ∈ 𝑋)))
35	34	rexlimdva 3135	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 → (𝑡 ∈ 𝑦 → 𝑡 ∈ 𝑋)))
36	35	com23 86	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑦 → (∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 → 𝑡 ∈ 𝑋)))
37	36	impd 410	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → ((𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧) → 𝑡 ∈ 𝑋))
38	37	rexlimdvw 3140	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧) → 𝑡 ∈ 𝑋))
39	28, 38	impbid 212	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑋 ↔ ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
40		elunirab 4889	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ↔ ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))
41	39, 40	bitr4di 289	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑋 ↔ 𝑡 ∈ ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧}))
42	41	eqrdv 2728	. . . . . . . . . . . . . 14 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → 𝑋 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧})
43		ssrab2 4046	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ⊆ (fi‘𝑥)
44		fvex 6874	. . . . . . . . . . . . . . . . 17 ⊢ (fi‘𝑥) ∈ V
45	44	elpw2 5292	. . . . . . . . . . . . . . . 16 ⊢ ({𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∈ 𝒫 (fi‘𝑥) ↔ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ⊆ (fi‘𝑥))
46	43, 45	mpbir 231	. . . . . . . . . . . . . . 15 ⊢ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∈ 𝒫 (fi‘𝑥)
47		unieq 4885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∪ 𝑎 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧})
48	47	eqeq2d 2741	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑋 = ∪ 𝑎 ↔ 𝑋 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧}))
49		pweq 4580	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → 𝒫 𝑎 = 𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧})
50	49	ineq1d 4185	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝒫 𝑎 ∩ Fin) = (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin))
51	50	rexeqdv 3302	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏 ↔ ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)𝑋 = ∪ 𝑏))
52	48, 51	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ((𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) ↔ (𝑋 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)𝑋 = ∪ 𝑏)))
53	52	rspcv 3587	. . . . . . . . . . . . . . 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 9312	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin) ↔ (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∧ 𝑏 ∈ Fin))
57		ssel 3943	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑡 ∈ 𝑏 → 𝑡 ∈ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧}))
58		sseq1 3975	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑡 → (𝑦 ⊆ 𝑧 ↔ 𝑡 ⊆ 𝑧))
59	58	rexbidv 3158	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑡 → (∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 ↔ ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧))
60	59	elrab 3662	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 ∈ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ↔ (𝑡 ∈ (fi‘𝑥) ∧ ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧))
61	60	simprbi 496	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧)
62	57, 61	syl6 35	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑡 ∈ 𝑏 → ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧))
63	62	ralrimiv 3125	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∀𝑡 ∈ 𝑏 ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧)
64		sseq2 3976	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = (𝑓‘𝑡) → (𝑡 ⊆ 𝑧 ↔ 𝑡 ⊆ (𝑓‘𝑡)))
65	64	ac6sfi 9238	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑏 ∈ Fin ∧ ∀𝑡 ∈ 𝑏 ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧) → ∃𝑓(𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)))
66	65	ex 412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ Fin → (∀𝑡 ∈ 𝑏 ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧 → ∃𝑓(𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡))))
67	63, 66	syl5 34	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ Fin → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∃𝑓(𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡))))
68	67	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∃𝑓(𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡))))
69		simprll 778	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑓:𝑏⟶𝑐)
70		frn 6698	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓:𝑏⟶𝑐 → ran 𝑓 ⊆ 𝑐)
71	69, 70	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ran 𝑓 ⊆ 𝑐)
72		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑏 ∈ Fin)
73		ffn 6691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓:𝑏⟶𝑐 → 𝑓 Fn 𝑏)
74		dffn4 6781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 Fn 𝑏 ↔ 𝑓:𝑏–onto→ran 𝑓)
75	73, 74	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:𝑏⟶𝑐 → 𝑓:𝑏–onto→ran 𝑓)
76	75	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) → 𝑓:𝑏–onto→ran 𝑓)
77	76	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑓:𝑏–onto→ran 𝑓)
78		fodomfi 9268	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑏 ∈ Fin ∧ 𝑓:𝑏–onto→ran 𝑓) → ran 𝑓 ≼ 𝑏)
79	72, 77, 78	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ran 𝑓 ≼ 𝑏)
80		domfi 9159	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 ∈ Fin ∧ ran 𝑓 ≼ 𝑏) → ran 𝑓 ∈ Fin)
81	72, 79, 80	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ran 𝑓 ∈ Fin)
82	71, 81	jca 511	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → (ran 𝑓 ⊆ 𝑐 ∧ ran 𝑓 ∈ Fin))
83		elin 3933	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ↔ (ran 𝑓 ∈ 𝒫 𝑐 ∧ ran 𝑓 ∈ Fin))
84		vex 3454	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑐 ∈ V
85	84	elpw2 5292	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ran 𝑓 ∈ 𝒫 𝑐 ↔ ran 𝑓 ⊆ 𝑐)
86	85	anbi1i 624	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ran 𝑓 ∈ 𝒫 𝑐 ∧ ran 𝑓 ∈ Fin) ↔ (ran 𝑓 ⊆ 𝑐 ∧ ran 𝑓 ∈ Fin))
87	83, 86	bitr2i 276	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ran 𝑓 ⊆ 𝑐 ∧ ran 𝑓 ∈ Fin) ↔ ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin))
88	82, 87	sylib 218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin))
89		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑋 = ∪ 𝑏)
90		uniiun 5025	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ∪ 𝑏 = ∪ 𝑡 ∈ 𝑏 𝑡
91		simprlr 779	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡))
92		ss2iun 4977	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡) → ∪ 𝑡 ∈ 𝑏 𝑡 ⊆ ∪ 𝑡 ∈ 𝑏 (𝑓‘𝑡))
93	91, 92	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ 𝑡 ∈ 𝑏 𝑡 ⊆ ∪ 𝑡 ∈ 𝑏 (𝑓‘𝑡))
94	90, 93	eqsstrid 3988	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ 𝑏 ⊆ ∪ 𝑡 ∈ 𝑏 (𝑓‘𝑡))
95		fniunfv 7224	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 Fn 𝑏 → ∪ 𝑡 ∈ 𝑏 (𝑓‘𝑡) = ∪ ran 𝑓)
96	69, 73, 95	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ 𝑡 ∈ 𝑏 (𝑓‘𝑡) = ∪ ran 𝑓)
97	94, 96	sseqtrd 3986	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ 𝑏 ⊆ ∪ ran 𝑓)
98	89, 97	eqsstrd 3984	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑋 ⊆ ∪ ran 𝑓)
99		simpll2 1214	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑐 ⊆ 𝐽)
100	71, 99	sstrd 3960	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ran 𝑓 ⊆ 𝐽)
101		uniss 4882	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ran 𝑓 ⊆ 𝐽 → ∪ ran 𝑓 ⊆ ∪ 𝐽)
102	101, 1	sseqtrrdi 3991	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ran 𝑓 ⊆ 𝐽 → ∪ ran 𝑓 ⊆ 𝑋)
103	100, 102	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ ran 𝑓 ⊆ 𝑋)
104	98, 103	eqssd 3967	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑋 = ∪ ran 𝑓)
105		unieq 4885	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = ran 𝑓 → ∪ 𝑑 = ∪ ran 𝑓)
106	105	eqeq2d 2741	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = ran 𝑓 → (𝑋 = ∪ 𝑑 ↔ 𝑋 = ∪ ran 𝑓))
107	106	rspcev 3591	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑋 = ∪ ran 𝑓) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)
108	88, 104, 107	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)
109	108	exp32 420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) → ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
110	109	exlimdv 1933	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) → (∃𝑓(𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
111	68, 110	syld 47	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
112	111	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑏 ∈ Fin → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))))
113	112	com23 86	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑏 ∈ Fin → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))))
114	113	impd 410	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → ((𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∧ 𝑏 ∈ Fin) → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
115	56, 114	biimtrid 242	. . . . . . . . . . . . . 14 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin) → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
116	115	rexlimdv 3133	. . . . . . . . . . . . 13 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))
117	55, 116	syld 47	. . . . . . . . . . . 12 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))
118	117	3exp 1119	. . . . . . . . . . 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 255	. . . . . . . 8 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → (𝑐 ∈ 𝒫 𝐽 → (𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))))
122	121	ralrimdv 3132	. . . . . . 7 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
123		fibas 22871	. . . . . . . . 9 ⊢ (fi‘𝑥) ∈ TopBases
124		tgcl 22863	. . . . . . . . 9 ⊢ ((fi‘𝑥) ∈ TopBases → (topGen‘(fi‘𝑥)) ∈ Top)
125	123, 124	ax-mp 5	. . . . . . . 8 ⊢ (topGen‘(fi‘𝑥)) ∈ Top
126		eleq1 2817	. . . . . . . 8 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (𝐽 ∈ Top ↔ (topGen‘(fi‘𝑥)) ∈ Top))
127	125, 126	mpbiri 258	. . . . . . 7 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → 𝐽 ∈ Top)
128	122, 127	jctild 525	. . . . . 6 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → (𝐽 ∈ Top ∧ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))))
129	1	iscmp 23282	. . . . . 6 ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
130	128, 129	imbitrrdi 252	. . . . 5 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → 𝐽 ∈ Comp))
131	3, 130	syld 47	. . . 4 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → 𝐽 ∈ Comp))
132	131	imp 406	. . 3 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)) → 𝐽 ∈ Comp)
133	132	exlimiv 1930	. 2 ⊢ (∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)) → 𝐽 ∈ Comp)
134	2, 133	impbii 209	1 ⊢ (𝐽 ∈ Comp ↔ ∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∀wral 3045  ∃wrex 3054  {crab 3408   ∩ cin 3916   ⊆ wss 3917  𝒫 cpw 4566  ∪ cuni 4874  ∪ ciun 4958   class class class wbr 5110  ran crn 5642   Fn wfn 6509  ⟶wf 6510  –onto→wfo 6512  ‘cfv 6514   ≼ cdom 8919  Fincfn 8921  ficfi 9368  topGenctg 17407  Topctop 22787  TopBasesctb 22839  Compccmp 23280

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-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-ac2 10423

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  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-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  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-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-se 5595  df-we 5596  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-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-isom 6523  df-riota 7347  df-ov 7393  df-rpss 7702  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-1o 8437  df-2o 8438  df-en 8922  df-dom 8923  df-fin 8925  df-fi 9369  df-card 9899  df-ac 10076  df-topgen 17413  df-top 22788  df-bases 22840  df-cmp 23281

This theorem is referenced by: (None)