Theorem alexsubALT 24245

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 24241	. 2 ⊢ (𝐽 ∈ Comp → ∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
3	1	alexsubALTlem4 24244	. . . . 5 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → ∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
4		velpw 4572	. . . . . . . . 9 ⊢ (𝑐 ∈ 𝒫 𝐽 ↔ 𝑐 ⊆ 𝐽)
5		eleq2 2855	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋 = ∪ 𝑐 → (𝑡 ∈ 𝑋 ↔ 𝑡 ∈ ∪ 𝑐))
6	5	3ad2ant3 1153	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑋 ↔ 𝑡 ∈ ∪ 𝑐))
7		eluni 4880	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ ∪ 𝑐 ↔ ∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑐))
8		ssel 3934	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑐 ⊆ 𝐽 → (𝑤 ∈ 𝑐 → 𝑤 ∈ 𝐽))
9		eleq2 2855	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (𝑤 ∈ 𝐽 ↔ 𝑤 ∈ (topGen‘(fi‘𝑥))))
10		tg2 23159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑤 ∈ (topGen‘(fi‘𝑥)) ∧ 𝑡 ∈ 𝑤) → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤))
11	10	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 ∈ (topGen‘(fi‘𝑥)) → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤)))
12	9, 11	biimtrdi 256	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (𝑤 ∈ 𝐽 → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤))))
13	8, 12	sylan9r 518	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → (𝑤 ∈ 𝑐 → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤))))
14	13	3impia 1135	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤)))
15		sseq2 3966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = 𝑤 → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑤))
16	15	rspcev 3584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑤 ∈ 𝑐 ∧ 𝑦 ⊆ 𝑤) → ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)
17	16	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 ∈ 𝑐 → (𝑦 ⊆ 𝑤 → ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))
18	17	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → (𝑦 ⊆ 𝑤 → ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))
19	18	anim2d 624	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → ((𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤) → (𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
20	19	reximdv 3183	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → (∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤) → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
21	14, 20	syld 48	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
22	21	3expia 1139	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → (𝑤 ∈ 𝑐 → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))))
23	22	com23 87	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → (𝑡 ∈ 𝑤 → (𝑤 ∈ 𝑐 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))))
24	23	impd 416	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → ((𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑐) → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
25	24	exlimdv 1966	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → (∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑐) → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
26	7, 25	biimtrid 245	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → (𝑡 ∈ ∪ 𝑐 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
27	26	3adant3 1150	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ ∪ 𝑐 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
28	6, 27	sylbid 243	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑋 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
29		ssel 3934	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ⊆ 𝑧 → (𝑡 ∈ 𝑦 → 𝑡 ∈ 𝑧))
30		elunii 4882	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ 𝑧 ∧ 𝑧 ∈ 𝑐) → 𝑡 ∈ ∪ 𝑐)
31	30	expcom 419	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ 𝑐 → (𝑡 ∈ 𝑧 → 𝑡 ∈ ∪ 𝑐))
32	6	biimprd 251	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ ∪ 𝑐 → 𝑡 ∈ 𝑋))
33	31, 32	sylan9r 518	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑧 ∈ 𝑐) → (𝑡 ∈ 𝑧 → 𝑡 ∈ 𝑋))
34	29, 33	syl9r 79	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑧 ∈ 𝑐) → (𝑦 ⊆ 𝑧 → (𝑡 ∈ 𝑦 → 𝑡 ∈ 𝑋)))
35	34	rexlimdva 3169	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 → (𝑡 ∈ 𝑦 → 𝑡 ∈ 𝑋)))
36	35	com23 87	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑦 → (∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 → 𝑡 ∈ 𝑋)))
37	36	impd 416	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → ((𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧) → 𝑡 ∈ 𝑋))
38	37	rexlimdvw 3174	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧) → 𝑡 ∈ 𝑋))
39	28, 38	impbid 215	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑋 ↔ ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
40		elunirab 4892	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ↔ ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))
41	39, 40	bitr4di 292	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑋 ↔ 𝑡 ∈ ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧}))
42	41	eqrdv 2764	. . . . . . . . . . . . . 14 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → 𝑋 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧})
43		ssrab2 4037	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ⊆ (fi‘𝑥)
44		fvex 6901	. . . . . . . . . . . . . . . . 17 ⊢ (fi‘𝑥) ∈ V
45	44	elpw2 5310	. . . . . . . . . . . . . . . 16 ⊢ ({𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∈ 𝒫 (fi‘𝑥) ↔ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ⊆ (fi‘𝑥))
46	43, 45	mpbir 234	. . . . . . . . . . . . . . 15 ⊢ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∈ 𝒫 (fi‘𝑥)
47		unieq 4888	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∪ 𝑎 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧})
48	47	eqeq2d 2777	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑋 = ∪ 𝑎 ↔ 𝑋 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧}))
49		pweq 4581	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → 𝒫 𝑎 = 𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧})
50	49	ineq1d 4175	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝒫 𝑎 ∩ Fin) = (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin))
51	50	rexeqdv 3327	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏 ↔ ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)𝑋 = ∪ 𝑏))
52	48, 51	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ((𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) ↔ (𝑋 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)𝑋 = ∪ 𝑏)))
53	52	rspcv 3580	. . . . . . . . . . . . . . 15 ⊢ ({𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∈ 𝒫 (fi‘𝑥) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → (𝑋 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)𝑋 = ∪ 𝑏)))
54	46, 53	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → (𝑋 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)𝑋 = ∪ 𝑏))
55	42, 54	syl5com 32	. . . . . . . . . . . . 13 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)𝑋 = ∪ 𝑏))
56		elfpw 9321	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin) ↔ (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∧ 𝑏 ∈ Fin))
57		ssel 3934	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑡 ∈ 𝑏 → 𝑡 ∈ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧}))
58		sseq1 3965	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑡 → (𝑦 ⊆ 𝑧 ↔ 𝑡 ⊆ 𝑧))
59	58	rexbidv 3192	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑡 → (∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 ↔ ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧))
60	59	elrab 3653	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 ∈ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ↔ (𝑡 ∈ (fi‘𝑥) ∧ ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧))
61	60	simprbi 503	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧)
62	57, 61	syl6 36	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑡 ∈ 𝑏 → ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧))
63	62	ralrimiv 3159	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∀𝑡 ∈ 𝑏 ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧)
64		sseq2 3966	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = (𝑓‘𝑡) → (𝑡 ⊆ 𝑧 ↔ 𝑡 ⊆ (𝑓‘𝑡)))
65	64	ac6sfi 9254	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑏 ∈ Fin ∧ ∀𝑡 ∈ 𝑏 ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧) → ∃𝑓(𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)))
66	65	ex 418	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ Fin → (∀𝑡 ∈ 𝑏 ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧 → ∃𝑓(𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡))))
67	63, 66	syl5 35	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ Fin → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∃𝑓(𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡))))
68	67	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∃𝑓(𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡))))
69		simprll 791	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑓:𝑏⟶𝑐)
70		frn 6720	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓:𝑏⟶𝑐 → ran 𝑓 ⊆ 𝑐)
71	69, 70	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ran 𝑓 ⊆ 𝑐)
72		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑏 ∈ Fin)
73		ffn 6712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓:𝑏⟶𝑐 → 𝑓 Fn 𝑏)
74		dffn4 6805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 Fn 𝑏 ↔ 𝑓:𝑏–onto→ran 𝑓)
75	73, 74	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:𝑏⟶𝑐 → 𝑓:𝑏–onto→ran 𝑓)
76	75	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) → 𝑓:𝑏–onto→ran 𝑓)
77	76	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑓:𝑏–onto→ran 𝑓)
78		fodomfi 9282	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑏 ∈ Fin ∧ 𝑓:𝑏–onto→ran 𝑓) → ran 𝑓 ≼ 𝑏)
79	72, 77, 78	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ran 𝑓 ≼ 𝑏)
80		domfi 9183	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 ∈ Fin ∧ ran 𝑓 ≼ 𝑏) → ran 𝑓 ∈ Fin)
81	72, 79, 80	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ran 𝑓 ∈ Fin)
82	71, 81	jca 521	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → (ran 𝑓 ⊆ 𝑐 ∧ ran 𝑓 ∈ Fin))
83		elin 3924	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ↔ (ran 𝑓 ∈ 𝒫 𝑐 ∧ ran 𝑓 ∈ Fin))
84		vex 3462	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑐 ∈ V
85	84	elpw2 5310	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ran 𝑓 ∈ 𝒫 𝑐 ↔ ran 𝑓 ⊆ 𝑐)
86	85	anbi1i 636	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ran 𝑓 ∈ 𝒫 𝑐 ∧ ran 𝑓 ∈ Fin) ↔ (ran 𝑓 ⊆ 𝑐 ∧ ran 𝑓 ∈ Fin))
87	83, 86	bitr2i 279	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ran 𝑓 ⊆ 𝑐 ∧ ran 𝑓 ∈ Fin) ↔ ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin))
88	82, 87	sylib 221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin))
89		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑋 = ∪ 𝑏)
90		uniiun 5028	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ∪ 𝑏 = ∪ 𝑡 ∈ 𝑏 𝑡
91		simprlr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡))
92		ss2iun 4980	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡) → ∪ 𝑡 ∈ 𝑏 𝑡 ⊆ ∪ 𝑡 ∈ 𝑏 (𝑓‘𝑡))
93	91, 92	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ 𝑡 ∈ 𝑏 𝑡 ⊆ ∪ 𝑡 ∈ 𝑏 (𝑓‘𝑡))
94	90, 93	eqsstrid 3978	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ 𝑏 ⊆ ∪ 𝑡 ∈ 𝑏 (𝑓‘𝑡))
95		fniunfv 7252	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 Fn 𝑏 → ∪ 𝑡 ∈ 𝑏 (𝑓‘𝑡) = ∪ ran 𝑓)
96	69, 73, 95	3syl 19	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ 𝑡 ∈ 𝑏 (𝑓‘𝑡) = ∪ ran 𝑓)
97	94, 96	sseqtrd 3976	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ 𝑏 ⊆ ∪ ran 𝑓)
98	89, 97	eqsstrd 3974	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑋 ⊆ ∪ ran 𝑓)
99		simpll2 1232	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑐 ⊆ 𝐽)
100	71, 99	sstrd 3950	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ran 𝑓 ⊆ 𝐽)
101		uniss 4885	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ran 𝑓 ⊆ 𝐽 → ∪ ran 𝑓 ⊆ ∪ 𝐽)
102	101, 1	sseqtrrdi 3981	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ran 𝑓 ⊆ 𝐽 → ∪ ran 𝑓 ⊆ 𝑋)
103	100, 102	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ ran 𝑓 ⊆ 𝑋)
104	98, 103	eqssd 3957	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑋 = ∪ ran 𝑓)
105		unieq 4888	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = ran 𝑓 → ∪ 𝑑 = ∪ ran 𝑓)
106	105	eqeq2d 2777	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = ran 𝑓 → (𝑋 = ∪ 𝑑 ↔ 𝑋 = ∪ ran 𝑓))
107	106	rspcev 3584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑋 = ∪ ran 𝑓) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)
108	88, 104, 107	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)
109	108	exp32 426	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) → ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
110	109	exlimdv 1966	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) → (∃𝑓(𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
111	68, 110	syld 48	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
112	111	ex 418	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑏 ∈ Fin → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))))
113	112	com23 87	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑏 ∈ Fin → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))))
114	113	impd 416	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → ((𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∧ 𝑏 ∈ Fin) → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
115	56, 114	biimtrid 245	. . . . . . . . . . . . . 14 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin) → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
116	115	rexlimdv 3167	. . . . . . . . . . . . 13 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))
117	55, 116	syld 48	. . . . . . . . . . . 12 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))
118	117	3exp 1137	. . . . . . . . . . 11 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (𝑐 ⊆ 𝐽 → (𝑋 = ∪ 𝑐 → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))))
119	118	com34 92	. . . . . . . . . 10 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (𝑐 ⊆ 𝐽 → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → (𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))))
120	119	com23 87	. . . . . . . . 9 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → (𝑐 ⊆ 𝐽 → (𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))))
121	4, 120	syl7bi 258	. . . . . . . 8 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → (𝑐 ∈ 𝒫 𝐽 → (𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))))
122	121	ralrimdv 3166	. . . . . . 7 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
123		fibas 23171	. . . . . . . . 9 ⊢ (fi‘𝑥) ∈ TopBases
124		tgcl 23163	. . . . . . . . 9 ⊢ ((fi‘𝑥) ∈ TopBases → (topGen‘(fi‘𝑥)) ∈ Top)
125	123, 124	ax-mp 5	. . . . . . . 8 ⊢ (topGen‘(fi‘𝑥)) ∈ Top
126		eleq1 2854	. . . . . . . 8 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (𝐽 ∈ Top ↔ (topGen‘(fi‘𝑥)) ∈ Top))
127	125, 126	mpbiri 261	. . . . . . 7 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → 𝐽 ∈ Top)
128	122, 127	jctild 535	. . . . . 6 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → (𝐽 ∈ Top ∧ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))))
129	1	iscmp 23582	. . . . . 6 ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
130	128, 129	imbitrrdi 255	. . . . 5 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → 𝐽 ∈ Comp))
131	3, 130	syld 48	. . . 4 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → 𝐽 ∈ Comp))
132	131	imp 412	. . 3 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)) → 𝐽 ∈ Comp)
133	132	exlimiv 1963	. 2 ⊢ (∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)) → 𝐽 ∈ Comp)
134	2, 133	impbii 212	1 ⊢ (𝐽 ∈ Comp ↔ ∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2146  ∀wral 3082  ∃wrex 3092  {crab 3419   ∩ cin 3907   ⊆ wss 3908  𝒫 cpw 4567  ∪ cuni 4877  ∪ ciun 4961   class class class wbr 5114  ran crn 5667   Fn wfn 6538  ⟶wf 6539  –onto→wfo 6541  ‘cfv 6543   ≼ cdom 8950  Fincfn 8952  ficfi 9380  topGenctg 17515  Topctop 23087  TopBasesctb 23139  Compccmp 23580

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-rep 5243  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-ac2 10465

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-int 4918  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-se 5620  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7380  df-ov 7426  df-rpss 7733  df-om 7872  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-1o 8462  df-2o 8463  df-en 8953  df-dom 8954  df-fin 8956  df-fi 9381  df-card 9944  df-ac 10119  df-topgen 17521  df-top 23088  df-bases 23140  df-cmp 23581

This theorem is used by: (None)