Theorem alexsubALT 24016

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 24012	. 2 ⊢ (𝐽 ∈ Comp → ∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
3	1	alexsubALTlem4 24015	. . . . 5 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → ∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
4		velpw 4546	. . . . . . . . 9 ⊢ (𝑐 ∈ 𝒫 𝐽 ↔ 𝑐 ⊆ 𝐽)
5		eleq2 2825	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋 = ∪ 𝑐 → (𝑡 ∈ 𝑋 ↔ 𝑡 ∈ ∪ 𝑐))
6	5	3ad2ant3 1136	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑋 ↔ 𝑡 ∈ ∪ 𝑐))
7		eluni 4853	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ ∪ 𝑐 ↔ ∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑐))
8		ssel 3915	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑐 ⊆ 𝐽 → (𝑤 ∈ 𝑐 → 𝑤 ∈ 𝐽))
9		eleq2 2825	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (𝑤 ∈ 𝐽 ↔ 𝑤 ∈ (topGen‘(fi‘𝑥))))
10		tg2 22930	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1118	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤)))
15		sseq2 3948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = 𝑤 → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑤))
16	15	rspcev 3564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑤 ∈ 𝑐 ∧ 𝑦 ⊆ 𝑤) → ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)
17	16	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 ∈ 𝑐 → (𝑦 ⊆ 𝑤 → ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))
18	17	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → (𝑦 ⊆ 𝑤 → ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))
19	18	anim2d 613	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → ((𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤) → (𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
20	19	reximdv 3152	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → (∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤) → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
21	14, 20	syld 47	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
22	21	3expia 1122	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → (𝑤 ∈ 𝑐 → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))))
23	22	com23 86	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → (𝑡 ∈ 𝑤 → (𝑤 ∈ 𝑐 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))))
24	23	impd 410	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → ((𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑐) → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
25	24	exlimdv 1935	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → (∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑐) → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
26	7, 25	biimtrid 242	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → (𝑡 ∈ ∪ 𝑐 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
27	26	3adant3 1133	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ ∪ 𝑐 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
28	6, 27	sylbid 240	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑋 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
29		ssel 3915	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ⊆ 𝑧 → (𝑡 ∈ 𝑦 → 𝑡 ∈ 𝑧))
30		elunii 4855	. . . . . . . . . . . . . . . . . . . . . . . 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 3138	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 → (𝑡 ∈ 𝑦 → 𝑡 ∈ 𝑋)))
36	35	com23 86	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑦 → (∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 → 𝑡 ∈ 𝑋)))
37	36	impd 410	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → ((𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧) → 𝑡 ∈ 𝑋))
38	37	rexlimdvw 3143	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧) → 𝑡 ∈ 𝑋))
39	28, 38	impbid 212	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑋 ↔ ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))
40		elunirab 4865	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ↔ ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))
41	39, 40	bitr4di 289	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑋 ↔ 𝑡 ∈ ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧}))
42	41	eqrdv 2734	. . . . . . . . . . . . . 14 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → 𝑋 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧})
43		ssrab2 4020	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ⊆ (fi‘𝑥)
44		fvex 6853	. . . . . . . . . . . . . . . . 17 ⊢ (fi‘𝑥) ∈ V
45	44	elpw2 5275	. . . . . . . . . . . . . . . 16 ⊢ ({𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∈ 𝒫 (fi‘𝑥) ↔ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ⊆ (fi‘𝑥))
46	43, 45	mpbir 231	. . . . . . . . . . . . . . 15 ⊢ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∈ 𝒫 (fi‘𝑥)
47		unieq 4861	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∪ 𝑎 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧})
48	47	eqeq2d 2747	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑋 = ∪ 𝑎 ↔ 𝑋 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧}))
49		pweq 4555	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → 𝒫 𝑎 = 𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧})
50	49	ineq1d 4159	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝒫 𝑎 ∩ Fin) = (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin))
51	50	rexeqdv 3296	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏 ↔ ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)𝑋 = ∪ 𝑏))
52	48, 51	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ((𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) ↔ (𝑋 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)𝑋 = ∪ 𝑏)))
53	52	rspcv 3560	. . . . . . . . . . . . . . 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 9264	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin) ↔ (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∧ 𝑏 ∈ Fin))
57		ssel 3915	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑡 ∈ 𝑏 → 𝑡 ∈ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧}))
58		sseq1 3947	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑡 → (𝑦 ⊆ 𝑧 ↔ 𝑡 ⊆ 𝑧))
59	58	rexbidv 3161	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑡 → (∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 ↔ ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧))
60	59	elrab 3634	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 ∈ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ↔ (𝑡 ∈ (fi‘𝑥) ∧ ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧))
61	60	simprbi 497	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧)
62	57, 61	syl6 35	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑡 ∈ 𝑏 → ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧))
63	62	ralrimiv 3128	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∀𝑡 ∈ 𝑏 ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧)
64		sseq2 3948	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = (𝑓‘𝑡) → (𝑡 ⊆ 𝑧 ↔ 𝑡 ⊆ (𝑓‘𝑡)))
65	64	ac6sfi 9194	. . . . . . . . . . . . . . . . . . . . . 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 779	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑓:𝑏⟶𝑐)
70		frn 6675	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓:𝑏⟶𝑐 → ran 𝑓 ⊆ 𝑐)
71	69, 70	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ran 𝑓 ⊆ 𝑐)
72		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑏 ∈ Fin)
73		ffn 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓:𝑏⟶𝑐 → 𝑓 Fn 𝑏)
74		dffn4 6758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 Fn 𝑏 ↔ 𝑓:𝑏–onto→ran 𝑓)
75	73, 74	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓:𝑏⟶𝑐 → 𝑓:𝑏–onto→ran 𝑓)
76	75	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) → 𝑓:𝑏–onto→ran 𝑓)
77	76	ad2antrl 729	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑓:𝑏–onto→ran 𝑓)
78		fodomfi 9222	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑏 ∈ Fin ∧ 𝑓:𝑏–onto→ran 𝑓) → ran 𝑓 ≼ 𝑏)
79	72, 77, 78	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ran 𝑓 ≼ 𝑏)
80		domfi 9123	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 ∈ Fin ∧ ran 𝑓 ≼ 𝑏) → ran 𝑓 ∈ Fin)
81	72, 79, 80	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ran 𝑓 ∈ Fin)
82	71, 81	jca 511	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → (ran 𝑓 ⊆ 𝑐 ∧ ran 𝑓 ∈ Fin))
83		elin 3905	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ↔ (ran 𝑓 ∈ 𝒫 𝑐 ∧ ran 𝑓 ∈ Fin))
84		vex 3433	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑐 ∈ V
85	84	elpw2 5275	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ran 𝑓 ∈ 𝒫 𝑐 ↔ ran 𝑓 ⊆ 𝑐)
86	85	anbi1i 625	. . . . . . . . . . . . . . . . . . . . . . . 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 773	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑋 = ∪ 𝑏)
90		uniiun 5001	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ∪ 𝑏 = ∪ 𝑡 ∈ 𝑏 𝑡
91		simprlr 780	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡))
92		ss2iun 4952	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡) → ∪ 𝑡 ∈ 𝑏 𝑡 ⊆ ∪ 𝑡 ∈ 𝑏 (𝑓‘𝑡))
93	91, 92	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ 𝑡 ∈ 𝑏 𝑡 ⊆ ∪ 𝑡 ∈ 𝑏 (𝑓‘𝑡))
94	90, 93	eqsstrid 3960	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ 𝑏 ⊆ ∪ 𝑡 ∈ 𝑏 (𝑓‘𝑡))
95		fniunfv 7202	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 Fn 𝑏 → ∪ 𝑡 ∈ 𝑏 (𝑓‘𝑡) = ∪ ran 𝑓)
96	69, 73, 95	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ 𝑡 ∈ 𝑏 (𝑓‘𝑡) = ∪ ran 𝑓)
97	94, 96	sseqtrd 3958	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ 𝑏 ⊆ ∪ ran 𝑓)
98	89, 97	eqsstrd 3956	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑋 ⊆ ∪ ran 𝑓)
99		simpll2 1215	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑐 ⊆ 𝐽)
100	71, 99	sstrd 3932	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ran 𝑓 ⊆ 𝐽)
101		uniss 4858	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ran 𝑓 ⊆ 𝐽 → ∪ ran 𝑓 ⊆ ∪ 𝐽)
102	101, 1	sseqtrrdi 3963	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ran 𝑓 ⊆ 𝐽 → ∪ ran 𝑓 ⊆ 𝑋)
103	100, 102	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ ran 𝑓 ⊆ 𝑋)
104	98, 103	eqssd 3939	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑋 = ∪ ran 𝑓)
105		unieq 4861	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = ran 𝑓 → ∪ 𝑑 = ∪ ran 𝑓)
106	105	eqeq2d 2747	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = ran 𝑓 → (𝑋 = ∪ 𝑑 ↔ 𝑋 = ∪ ran 𝑓))
107	106	rspcev 3564	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑋 = ∪ ran 𝑓) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)
108	88, 104, 107	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)
109	108	exp32 420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) → ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
110	109	exlimdv 1935	. . . . . . . . . . . . . . . . . . 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 3136	. . . . . . . . . . . . 13 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))
117	55, 116	syld 47	. . . . . . . . . . . 12 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))
118	117	3exp 1120	. . . . . . . . . . 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 3135	. . . . . . 7 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
123		fibas 22942	. . . . . . . . 9 ⊢ (fi‘𝑥) ∈ TopBases
124		tgcl 22934	. . . . . . . . 9 ⊢ ((fi‘𝑥) ∈ TopBases → (topGen‘(fi‘𝑥)) ∈ Top)
125	123, 124	ax-mp 5	. . . . . . . 8 ⊢ (topGen‘(fi‘𝑥)) ∈ Top
126		eleq1 2824	. . . . . . . 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 23353	. . . . . 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 1932	. 2 ⊢ (∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)) → 𝐽 ∈ Comp)
134	2, 133	impbii 209	1 ⊢ (𝐽 ∈ Comp ↔ ∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∀wral 3051  ∃wrex 3061  {crab 3389   ∩ cin 3888   ⊆ wss 3889  𝒫 cpw 4541  ∪ cuni 4850  ∪ ciun 4933   class class class wbr 5085  ran crn 5632   Fn wfn 6493  ⟶wf 6494  –onto→wfo 6496  ‘cfv 6498   ≼ cdom 8891  Fincfn 8893  ficfi 9323  topGenctg 17400  Topctop 22858  TopBasesctb 22910  Compccmp 23351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-ac2 10385

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-int 4890  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-isom 6507  df-riota 7324  df-ov 7370  df-rpss 7677  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-1o 8405  df-2o 8406  df-en 8894  df-dom 8895  df-fin 8897  df-fi 9324  df-card 9863  df-ac 10038  df-topgen 17406  df-top 22859  df-bases 22911  df-cmp 23352

This theorem is referenced by: (None)