Theorem alexsubALTlem3 24348

Description: Lemma for alexsubALT 24350. If a point is covered by a collection taken from the base with no finite subcover, a set from the subbase can be added that covers the point so that the resulting collection has no finite subcover. (Contributed by Jeff Hankins, 28-Jan-2010.) (Revised by Mario Carneiro, 14-Dec-2013.)

Hypothesis

Ref	Expression
alexsubALT.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
alexsubALTlem3	⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)

Distinct variable groups:   𝑎,𝑏,𝑐,𝑑,𝑛,𝑠,𝑡,𝑢,𝑤,𝑥,𝑦,𝐽   𝑋,𝑎,𝑏,𝑐,𝑑,𝑛,𝑠,𝑡,𝑢,𝑤,𝑥,𝑦

Proof of Theorem alexsubALTlem3

Dummy variables 𝑓 𝑚 𝑣 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfrex2 3090	. . . . . . . . . . 11 ⊢ (∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛 ↔ ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)
2	1	ralbii 3109	. . . . . . . . . 10 ⊢ (∀𝑠 ∈ 𝑡 ∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛 ↔ ∀𝑠 ∈ 𝑡 ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)
3		ralnex 3089	. . . . . . . . . 10 ⊢ (∀𝑠 ∈ 𝑡 ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛 ↔ ¬ ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)
4	2, 3	bitr2i 279	. . . . . . . . 9 ⊢ (¬ ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛 ↔ ∀𝑠 ∈ 𝑡 ∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛)
5		elin 3915	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ↔ (𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin))
6		elpwi 4564	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) → 𝑛 ⊆ (𝑢 ∪ {𝑠}))
7	6	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → 𝑛 ⊆ (𝑢 ∪ {𝑠}))
8		uncom 4105	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∪ {𝑠}) = ({𝑠} ∪ 𝑢)
9	7, 8	sseqtrdi 3971	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → 𝑛 ⊆ ({𝑠} ∪ 𝑢))
10		ssundif 4443	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ⊆ ({𝑠} ∪ 𝑢) ↔ (𝑛 ∖ {𝑠}) ⊆ 𝑢)
11	9, 10	sylib 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → (𝑛 ∖ {𝑠}) ⊆ 𝑢)
12		diffi 9174	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ Fin → (𝑛 ∖ {𝑠}) ∈ Fin)
13	12	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → (𝑛 ∖ {𝑠}) ∈ Fin)
14	11, 13	jca 521	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
15	5, 14	sylbi 220	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
16	15	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
17	16	ad2antll 742	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
18		elin 3915	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
19		vex 3455	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑢 ∈ V
20	19	elpw2 5296	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ↔ (𝑛 ∖ {𝑠}) ⊆ 𝑢)
21	20	anbi1i 636	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin) ↔ ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
22	18, 21	bitr2i 279	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin) ↔ (𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin))
23	17, 22	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → (𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin))
24		simprrr 794	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑋 = ∪ 𝑛)
25		eldif 3909	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝑛 ∖ {𝑠}) ↔ (𝑥 ∈ 𝑛 ∧ ¬ 𝑥 ∈ {𝑠}))
26	25	simplbi2 506	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ 𝑛 → (¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})))
27		elun 4100	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) ↔ (𝑥 ∈ (𝑛 ∖ {𝑠}) ∨ 𝑥 ∈ {𝑠}))
28		orcom 884	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ (𝑥 ∈ (𝑛 ∖ {𝑠}) ∨ 𝑥 ∈ {𝑠}))
29	27, 28	bitr4i 281	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) ↔ (𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})))
30		df-or 862	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ (¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})))
31	29, 30	bitr2i 279	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ 𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
32	26, 31	sylib 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝑛 → 𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
33	32	ssriv 3935	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑛 ⊆ ((𝑛 ∖ {𝑠}) ∪ {𝑠})
34		uniss 4875	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ⊆ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) → ∪ 𝑛 ⊆ ∪ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
35	33, 34	mp1i 14	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑛 ⊆ ∪ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
36		uniun 4890	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) = (∪ (𝑛 ∖ {𝑠}) ∪ ∪ {𝑠})
37		unisnv 4887	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ {𝑠} = 𝑠
38	37	uneq2i 4112	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ (𝑛 ∖ {𝑠}) ∪ ∪ {𝑠}) = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠)
39	36, 38	eqtri 2784	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠)
40	35, 39	sseqtrdi 3971	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑛 ⊆ (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠))
41	24, 40	eqsstrd 3965	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑋 ⊆ (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠))
42		difss 4083	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∖ {𝑠}) ⊆ 𝑛
43	42	unissi 4876	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ (𝑛 ∖ {𝑠}) ⊆ ∪ 𝑛
44		sseq2 3957	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑋 = ∪ 𝑛 → (∪ (𝑛 ∖ {𝑠}) ⊆ 𝑋 ↔ ∪ (𝑛 ∖ {𝑠}) ⊆ ∪ 𝑛))
45	43, 44	mpbiri 261	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋 = ∪ 𝑛 → ∪ (𝑛 ∖ {𝑠}) ⊆ 𝑋)
46	45	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛) → ∪ (𝑛 ∖ {𝑠}) ⊆ 𝑋)
47	46	ad2antll 742	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ (𝑛 ∖ {𝑠}) ⊆ 𝑋)
48		elinel1 4147	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ 𝒫 𝑥)
49	48	elpwid 4566	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ⊆ 𝑥)
50	49	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢) → 𝑡 ⊆ 𝑥)
51	50	ad2antlr 740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑡 ⊆ 𝑥)
52		simprl 783	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑠 ∈ 𝑡)
53	51, 52	sseldd 3932	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑠 ∈ 𝑥)
54		elssuni 4899	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ 𝑥 → 𝑠 ⊆ ∪ 𝑥)
55	53, 54	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑠 ⊆ ∪ 𝑥)
56		fibas 23275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (fi‘𝑥) ∈ TopBases
57		unitg 23265	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((fi‘𝑥) ∈ TopBases → ∪ (topGen‘(fi‘𝑥)) = ∪ (fi‘𝑥))
58	56, 57	mp1i 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ (topGen‘(fi‘𝑥)) = ∪ (fi‘𝑥))
59		unieq 4878	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → ∪ 𝐽 = ∪ (topGen‘(fi‘𝑥)))
60	59	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → ∪ 𝐽 = ∪ (topGen‘(fi‘𝑥)))
61	60	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝐽 = ∪ (topGen‘(fi‘𝑥)))
62		vex 3455	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ∈ V
63		fiuni 9404	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ V → ∪ 𝑥 = ∪ (fi‘𝑥))
64	62, 63	mp1i 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑥 = ∪ (fi‘𝑥))
65	58, 61, 64	3eqtr4rd 2807	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑥 = ∪ 𝐽)
66		alexsubALT.1	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑋 = ∪ 𝐽
67	65, 66	eqtr4di 2814	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑥 = 𝑋)
68	55, 67	sseqtrd 3967	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑠 ⊆ 𝑋)
69	47, 68	unssd 4138	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠) ⊆ 𝑋)
70	41, 69	eqssd 3948	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑋 = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠))
71		unieq 4878	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝑛 ∖ {𝑠}) → ∪ 𝑚 = ∪ (𝑛 ∖ {𝑠}))
72	71	uneq1d 4114	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝑛 ∖ {𝑠}) → (∪ 𝑚 ∪ 𝑠) = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠))
73	72	rspceeqv 3599	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠)) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠))
74	23, 70, 73	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠))
75	74	expr 462	. . . . . . . . . . . . 13 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ 𝑠 ∈ 𝑡) → ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠)))
76	75	expd 421	. . . . . . . . . . . 12 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ 𝑠 ∈ 𝑡) → (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) → (𝑋 = ∪ 𝑛 → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠))))
77	76	rexlimdv 3162	. . . . . . . . . . 11 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ 𝑠 ∈ 𝑡) → (∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛 → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠)))
78	77	ralimdva 3175	. . . . . . . . . 10 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (∀𝑠 ∈ 𝑡 ∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛 → ∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠)))
79		elinel2 4148	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ Fin)
80	79	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) → 𝑡 ∈ Fin)
81		unieq 4878	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝑓‘𝑠) → ∪ 𝑚 = ∪ (𝑓‘𝑠))
82	81	uneq1d 4114	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝑓‘𝑠) → (∪ 𝑚 ∪ 𝑠) = (∪ (𝑓‘𝑠) ∪ 𝑠))
83	82	eqeq2d 2772	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝑓‘𝑠) → (𝑋 = (∪ 𝑚 ∪ 𝑠) ↔ 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)))
84	83	ac6sfi 9259	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ Fin ∧ ∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠)) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)))
85	84	ex 418	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ Fin → (∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))))
86	80, 85	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) → (∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))))
87	86	adantr 486	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) → (∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))))
88	87	ad2antrl 741	. . . . . . . . . 10 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))))
89		ffvelcdm 7073	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠 ∈ 𝑡) → (𝑓‘𝑠) ∈ (𝒫 𝑢 ∩ Fin))
90		elin 3915	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓‘𝑠) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((𝑓‘𝑠) ∈ 𝒫 𝑢 ∧ (𝑓‘𝑠) ∈ Fin))
91		elpwi 4564	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓‘𝑠) ∈ 𝒫 𝑢 → (𝑓‘𝑠) ⊆ 𝑢)
92	91	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓‘𝑠) ∈ 𝒫 𝑢 ∧ (𝑓‘𝑠) ∈ Fin) → (𝑓‘𝑠) ⊆ 𝑢)
93	90, 92	sylbi 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓‘𝑠) ∈ (𝒫 𝑢 ∩ Fin) → (𝑓‘𝑠) ⊆ 𝑢)
94	89, 93	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠 ∈ 𝑡) → (𝑓‘𝑠) ⊆ 𝑢)
95	94	ralrimiva 3155	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∀𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢)
96		iunss 5003	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢 ↔ ∀𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢)
97	95, 96	sylibr 237	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢)
98	97	ad2antrl 741	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢)
99		simplrr 790	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑤 ∈ 𝑢)
100	99	snssd 4747	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → {𝑤} ⊆ 𝑢)
101	98, 100	unssd 4138	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑢)
102	89	elin2d 4151	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠 ∈ 𝑡) → (𝑓‘𝑠) ∈ Fin)
103	102	ralrimiva 3155	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∀𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
104		iunfi 9316	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ Fin ∧ ∀𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
105	80, 103, 104	syl2an 608	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin)) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
106	105	ad4ant14 765	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢) ∧ 𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin)) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
107	106	ad2ant2lr 761	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
108		snfi 9055	. . . . . . . . . . . . . . . 16 ⊢ {𝑤} ∈ Fin
109		unfi 9170	. . . . . . . . . . . . . . . 16 ⊢ ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin ∧ {𝑤} ∈ Fin) → (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin)
110	107, 108, 109	sylancl 598	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin)
111	101, 110	jca 521	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin))
112		elin 3915	. . . . . . . . . . . . . . 15 ⊢ ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ∧ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin))
113	19	elpw2 5296	. . . . . . . . . . . . . . . 16 ⊢ ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ↔ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑢)
114	113	anbi1i 636	. . . . . . . . . . . . . . 15 ⊢ (((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ∧ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin) ↔ ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin))
115	112, 114	bitr2i 279	. . . . . . . . . . . . . 14 ⊢ (((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin) ↔ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin))
116	111, 115	sylib 221	. . . . . . . . . . . . 13 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin))
117		ralnex 3089	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠))
118	117	imbi2i 339	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) ↔ (𝑣 ∈ 𝑦 → ¬ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)))
119	118	albii 1852	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) ↔ ∀𝑦(𝑣 ∈ 𝑦 → ¬ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)))
120		alinexa 1876	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦(𝑣 ∈ 𝑦 → ¬ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ↔ ¬ ∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)))
121	119, 120	bitr2i 279	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ ∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ↔ ∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)))
122		fveq2 6877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑠 = 𝑧 → (𝑓‘𝑠) = (𝑓‘𝑧))
123	122	unieqd 4880	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑠 = 𝑧 → ∪ (𝑓‘𝑠) = ∪ (𝑓‘𝑧))
124		id 23	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑠 = 𝑧 → 𝑠 = 𝑧)
125	123, 124	uneq12d 4116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑠 = 𝑧 → (∪ (𝑓‘𝑠) ∪ 𝑠) = (∪ (𝑓‘𝑧) ∪ 𝑧))
126	125	eqeq2d 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑠 = 𝑧 → (𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) ↔ 𝑋 = (∪ (𝑓‘𝑧) ∪ 𝑧)))
127	126	rspcv 3573	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ 𝑡 → (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → 𝑋 = (∪ (𝑓‘𝑧) ∪ 𝑧)))
128		eleq2 2850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑋 = (∪ (𝑓‘𝑧) ∪ 𝑧) → (𝑣 ∈ 𝑋 ↔ 𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧)))
129	128	biimpd 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑋 = (∪ (𝑓‘𝑧) ∪ 𝑧) → (𝑣 ∈ 𝑋 → 𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧)))
130		elun 4100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧) ↔ (𝑣 ∈ ∪ (𝑓‘𝑧) ∨ 𝑣 ∈ 𝑧))
131		eluni 4870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑣 ∈ ∪ (𝑓‘𝑧) ↔ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)))
132	131	orbi1i 927	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑣 ∈ ∪ (𝑓‘𝑧) ∨ 𝑣 ∈ 𝑧) ↔ (∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) ∨ 𝑣 ∈ 𝑧))
133		df-or 862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) ∨ 𝑣 ∈ 𝑧) ↔ (¬ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧))
134		alinexa 1876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧)) ↔ ¬ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)))
135	134	imbi1i 352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧) ↔ (¬ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧))
136	133, 135	bitr4i 281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) ∨ 𝑣 ∈ 𝑧) ↔ (∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧))
137	130, 132, 136	3bitri 300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧) ↔ (∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧))
138		eleq2 2850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 = 𝑤 → (𝑣 ∈ 𝑦 ↔ 𝑣 ∈ 𝑤))
139		eleq1w 2844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ (𝑓‘𝑠) ↔ 𝑤 ∈ (𝑓‘𝑠)))
140	139	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 = 𝑤 → (¬ 𝑦 ∈ (𝑓‘𝑠) ↔ ¬ 𝑤 ∈ (𝑓‘𝑠)))
141	140	ralbidv 3186	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 = 𝑤 → (∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠) ↔ ∀𝑠 ∈ 𝑡 ¬ 𝑤 ∈ (𝑓‘𝑠)))
142	138, 141	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 = 𝑤 → ((𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) ↔ (𝑣 ∈ 𝑤 → ∀𝑠 ∈ 𝑡 ¬ 𝑤 ∈ (𝑓‘𝑠))))
143	142	spvv 2021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → (𝑣 ∈ 𝑤 → ∀𝑠 ∈ 𝑡 ¬ 𝑤 ∈ (𝑓‘𝑠)))
144	122	eleq2d 2847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑠 = 𝑧 → (𝑤 ∈ (𝑓‘𝑠) ↔ 𝑤 ∈ (𝑓‘𝑧)))
145	144	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑠 = 𝑧 → (¬ 𝑤 ∈ (𝑓‘𝑠) ↔ ¬ 𝑤 ∈ (𝑓‘𝑧)))
146	145	rspcv 3573	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 ∈ 𝑡 → (∀𝑠 ∈ 𝑡 ¬ 𝑤 ∈ (𝑓‘𝑠) → ¬ 𝑤 ∈ (𝑓‘𝑧)))
147	143, 146	syl9r 79	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → (𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧))))
148	147	alrimdv 1962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 ∈ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → ∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧))))
149	148	imim1d 83	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 ∈ 𝑡 → ((∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑧)))
150	137, 149	biimtrid 245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 ∈ 𝑡 → (𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑧)))
151	150	a1dd 51	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 ∈ 𝑡 → (𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧) → (𝑤 = ∩ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑧))))
152	129, 151	syl9r 79	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ 𝑡 → (𝑋 = (∪ (𝑓‘𝑧) ∪ 𝑧) → (𝑣 ∈ 𝑋 → (𝑤 = ∩ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑧)))))
153	127, 152	syld 48	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ 𝑡 → (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (𝑣 ∈ 𝑋 → (𝑤 = ∩ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑧)))))
154	153	com14 97	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = ∩ 𝑡 → (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (𝑣 ∈ 𝑋 → (𝑧 ∈ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑧)))))
155	154	imp31 423	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (𝑧 ∈ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑧)))
156	155	com23 87	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → (𝑧 ∈ 𝑡 → 𝑣 ∈ 𝑧)))
157	156	ralrimdv 3161	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → ∀𝑧 ∈ 𝑡 𝑣 ∈ 𝑧))
158		vex 3455	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑣 ∈ V
159	158	elint2 4914	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ ∩ 𝑡 ↔ ∀𝑧 ∈ 𝑡 𝑣 ∈ 𝑧)
160	157, 159	imbitrrdi 255	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ ∩ 𝑡))
161		eleq2 2850	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = ∩ 𝑡 → (𝑣 ∈ 𝑤 ↔ 𝑣 ∈ ∩ 𝑡))
162	161	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (𝑣 ∈ 𝑤 ↔ 𝑣 ∈ ∩ 𝑡))
163	160, 162	sylibrd 262	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑤))
164	121, 163	biimtrid 245	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (¬ ∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑤))
165	164	orrd 877	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ∨ 𝑣 ∈ 𝑤))
166	165	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → (𝑣 ∈ 𝑋 → (∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ∨ 𝑣 ∈ 𝑤)))
167		orc 881	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) → (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤))
168	167	anim2i 629	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) → (𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
169	168	eximi 1868	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) → ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
170		equid 2045	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑤 = 𝑤
171		vex 3455	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑤 ∈ V
172		equequ1 2058	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑤 → (𝑦 = 𝑤 ↔ 𝑤 = 𝑤))
173	138, 172	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑤 → ((𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤) ↔ (𝑣 ∈ 𝑤 ∧ 𝑤 = 𝑤)))
174	171, 173	spcev 3561	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑣 ∈ 𝑤 ∧ 𝑤 = 𝑤) → ∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤))
175	170, 174	mpan2 704	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ 𝑤 → ∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤))
176		olc 882	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑤 → (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤))
177	176	anim2i 629	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤) → (𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
178	177	eximi 1868	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤) → ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
179	175, 178	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ 𝑤 → ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
180	169, 179	jaoi 871	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ∨ 𝑣 ∈ 𝑤) → ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
181		eluni 4870	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ ∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})))
182		elun 4100	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ (𝑦 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∨ 𝑦 ∈ {𝑤}))
183		eliun 4955	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ↔ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠))
184		velsn 4600	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ {𝑤} ↔ 𝑦 = 𝑤)
185	183, 184	orbi12i 928	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∨ 𝑦 ∈ {𝑤}) ↔ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤))
186	182, 185	bitri 278	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤))
187	186	anbi2i 635	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑣 ∈ 𝑦 ∧ 𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})) ↔ (𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
188	187	exbii 1881	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})) ↔ ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
189	181, 188	bitr2i 279	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)) ↔ 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
190	180, 189	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ ((∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ∨ 𝑣 ∈ 𝑤) → 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
191	166, 190	syl6 36	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → (𝑣 ∈ 𝑋 → 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})))
192	191	ad5ant25 774	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → (𝑣 ∈ 𝑋 → 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})))
193	192	ad2ant2l 759	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (𝑣 ∈ 𝑋 → 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})))
194	193	ssrdv 3937	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑋 ⊆ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
195		elun 4100	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ (𝑣 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∨ 𝑣 ∈ {𝑤}))
196		eliun 4955	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ↔ ∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠))
197		velsn 4600	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ∈ {𝑤} ↔ 𝑣 = 𝑤)
198	196, 197	orbi12i 928	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∨ 𝑣 ∈ {𝑤}) ↔ (∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) ∨ 𝑣 = 𝑤))
199	195, 198	bitri 278	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ (∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) ∨ 𝑣 = 𝑤))
200		nfra1 3287	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑠∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)
201		nfv 1947	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑠 𝑣 ⊆ 𝑋
202		rsp 3251	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (𝑠 ∈ 𝑡 → 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)))
203		eqimss2 3990	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (∪ (𝑓‘𝑠) ∪ 𝑠) ⊆ 𝑋)
204		elssuni 4899	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ ∪ (𝑓‘𝑠))
205		ssun3 4126	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ⊆ ∪ (𝑓‘𝑠) → 𝑣 ⊆ (∪ (𝑓‘𝑠) ∪ 𝑠))
206	204, 205	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ (∪ (𝑓‘𝑠) ∪ 𝑠))
207		sstr 3939	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 ⊆ (∪ (𝑓‘𝑠) ∪ 𝑠) ∧ (∪ (𝑓‘𝑠) ∪ 𝑠) ⊆ 𝑋) → 𝑣 ⊆ 𝑋)
208	207	expcom 419	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((∪ (𝑓‘𝑠) ∪ 𝑠) ⊆ 𝑋 → (𝑣 ⊆ (∪ (𝑓‘𝑠) ∪ 𝑠) → 𝑣 ⊆ 𝑋))
209	203, 206, 208	syl2im 41	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ 𝑋))
210	202, 209	syl6 36	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (𝑠 ∈ 𝑡 → (𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ 𝑋)))
211	200, 201, 210	rexlimd 3270	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ 𝑋))
212	211	ad2antll 742	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ 𝑋))
213		elpwi 4564	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑢 ∈ 𝒫 (fi‘𝑥) → 𝑢 ⊆ (fi‘𝑥))
214	213	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) → 𝑢 ⊆ (fi‘𝑥))
215	214	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑢 ⊆ (fi‘𝑥))
216	215, 99	sseldd 3932	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑤 ∈ (fi‘𝑥))
217		elssuni 4899	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ (fi‘𝑥) → 𝑤 ⊆ ∪ (fi‘𝑥))
218	216, 217	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑤 ⊆ ∪ (fi‘𝑥))
219	56, 57	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ (topGen‘(fi‘𝑥)) = ∪ (fi‘𝑥)
220	59, 219	eqtr2di 2813	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → ∪ (fi‘𝑥) = ∪ 𝐽)
221	220, 66	eqtr4di 2814	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → ∪ (fi‘𝑥) = 𝑋)
222	221	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → ∪ (fi‘𝑥) = 𝑋)
223	222	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∪ (fi‘𝑥) = 𝑋)
224	218, 223	sseqtrd 3967	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑤 ⊆ 𝑋)
225		sseq1 3956	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = 𝑤 → (𝑣 ⊆ 𝑋 ↔ 𝑤 ⊆ 𝑋))
226	224, 225	syl5ibrcom 250	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (𝑣 = 𝑤 → 𝑣 ⊆ 𝑋))
227	212, 226	jaod 873	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ((∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) ∨ 𝑣 = 𝑤) → 𝑣 ⊆ 𝑋))
228	199, 227	biimtrid 245	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) → 𝑣 ⊆ 𝑋))
229	228	ralrimiv 3154	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∀𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})𝑣 ⊆ 𝑋)
230		unissb 4901	. . . . . . . . . . . . . . 15 ⊢ (∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑋 ↔ ∀𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})𝑣 ⊆ 𝑋)
231	229, 230	sylibr 237	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑋)
232	194, 231	eqssd 3948	. . . . . . . . . . . . 13 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑋 = ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
233		unieq 4878	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) → ∪ 𝑏 = ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
234	233	rspceeqv 3599	. . . . . . . . . . . . 13 ⊢ (((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏)
235	116, 232, 234	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏)
236	235	ex 418	. . . . . . . . . . 11 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏))
237	236	exlimdv 1966	. . . . . . . . . 10 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏))
238	78, 88, 237	3syld 61	. . . . . . . . 9 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (∀𝑠 ∈ 𝑡 ∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛 → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏))
239	4, 238	biimtrid 245	. . . . . . . 8 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (¬ ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛 → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏))
240		dfrex2 3090	. . . . . . . 8 ⊢ (∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏 ↔ ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)
241	239, 240	imbitrdi 254	. . . . . . 7 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (¬ ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛 → ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))
242	241	con4d 116	. . . . . 6 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))
243	242	exp32 426	. . . . 5 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) → (𝑤 ∈ 𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))))
244	243	com24 96	. . . 4 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → (𝑤 ∈ 𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))))
245	244	exp32 426	. . 3 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (𝑢 ∈ 𝒫 (fi‘𝑥) → (𝑎 ⊆ 𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → (𝑤 ∈ 𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))))))
246	245	imp45 435	. 2 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑤 ∈ 𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)))
247	246	imp31 423	1 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∀wral 3077  ∃wrex 3087  Vcvv 3451   ∖ cdif 3896   ∪ cun 3897   ∩ cin 3898   ⊆ wss 3899  𝒫 cpw 4557  {csn 4584  ∪ cuni 4867  ∩ cint 4907  ∪ ciun 4951  ⟶wf 6527  ‘cfv 6531  Fincfn 8957  ficfi 9386  topGenctg 17588  TopBasesctb 23243

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-om 7867  df-1o 8460  df-2o 8461  df-en 8958  df-fin 8961  df-fi 9387  df-topgen 17594  df-bases 23244

This theorem is used by:  alexsubALTlem4  24349