Theorem alexsubALTlem3 21663

Description: Lemma for alexsubALT 21665. 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 2979	. . . . . . . . . . 11 ⊢ (∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛 ↔ ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)
2	1	ralbii 2963	. . . . . . . . . 10 ⊢ (∀𝑠 ∈ 𝑡 ∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛 ↔ ∀𝑠 ∈ 𝑡 ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)
3		ralnex 2975	. . . . . . . . . 10 ⊢ (∀𝑠 ∈ 𝑡 ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛 ↔ ¬ ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)
4	2, 3	bitr2i 264	. . . . . . . . 9 ⊢ (¬ ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛 ↔ ∀𝑠 ∈ 𝑡 ∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛)
5		elin 3758	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ↔ (𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin))
6		elpwi 4117	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) → 𝑛 ⊆ (𝑢 ∪ {𝑠}))
7	6	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → 𝑛 ⊆ (𝑢 ∪ {𝑠}))
8		uncom 3719	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∪ {𝑠}) = ({𝑠} ∪ 𝑢)
9	7, 8	syl6sseq 3614	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → 𝑛 ⊆ ({𝑠} ∪ 𝑢))
10		ssundif 4004	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ⊆ ({𝑠} ∪ 𝑢) ↔ (𝑛 ∖ {𝑠}) ⊆ 𝑢)
11	9, 10	sylib 207	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → (𝑛 ∖ {𝑠}) ⊆ 𝑢)
12		diffi 8077	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ Fin → (𝑛 ∖ {𝑠}) ∈ Fin)
13	12	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → (𝑛 ∖ {𝑠}) ∈ Fin)
14	11, 13	jca 553	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
15	5, 14	sylbi 206	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
16	15	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
17	16	ad2antll 761	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
18		elin 3758	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
19		vex 3176	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑢 ∈ V
20	19	elpw2 4755	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ↔ (𝑛 ∖ {𝑠}) ⊆ 𝑢)
21	20	anbi1i 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin) ↔ ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
22	18, 21	bitr2i 264	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin) ↔ (𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin))
23	17, 22	sylib 207	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → (𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin))
24		simprrr 801	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑋 = ∪ 𝑛)
25		eldif 3550	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝑛 ∖ {𝑠}) ↔ (𝑥 ∈ 𝑛 ∧ ¬ 𝑥 ∈ {𝑠}))
26	25	simplbi2 653	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ 𝑛 → (¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})))
27		elun 3715	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) ↔ (𝑥 ∈ (𝑛 ∖ {𝑠}) ∨ 𝑥 ∈ {𝑠}))
28		orcom 401	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ (𝑥 ∈ (𝑛 ∖ {𝑠}) ∨ 𝑥 ∈ {𝑠}))
29	27, 28	bitr4i 266	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) ↔ (𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})))
30		df-or 384	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ (¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})))
31	29, 30	bitr2i 264	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ 𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
32	26, 31	sylib 207	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝑛 → 𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
33	32	ssriv 3572	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑛 ⊆ ((𝑛 ∖ {𝑠}) ∪ {𝑠})
34		uniss 4394	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ⊆ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) → ∪ 𝑛 ⊆ ∪ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
35	33, 34	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑛 ⊆ ∪ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
36		uniun 4392	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) = (∪ (𝑛 ∖ {𝑠}) ∪ ∪ {𝑠})
37		vex 3176	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑠 ∈ V
38	37	unisn 4387	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ {𝑠} = 𝑠
39	38	uneq2i 3726	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ (𝑛 ∖ {𝑠}) ∪ ∪ {𝑠}) = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠)
40	36, 39	eqtri 2632	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠)
41	35, 40	syl6sseq 3614	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑛 ⊆ (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠))
42	24, 41	eqsstrd 3602	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑋 ⊆ (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠))
43		difss 3699	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∖ {𝑠}) ⊆ 𝑛
44	43	unissi 4397	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ (𝑛 ∖ {𝑠}) ⊆ ∪ 𝑛
45		sseq2 3590	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑋 = ∪ 𝑛 → (∪ (𝑛 ∖ {𝑠}) ⊆ 𝑋 ↔ ∪ (𝑛 ∖ {𝑠}) ⊆ ∪ 𝑛))
46	44, 45	mpbiri 247	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋 = ∪ 𝑛 → ∪ (𝑛 ∖ {𝑠}) ⊆ 𝑋)
47	46	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛) → ∪ (𝑛 ∖ {𝑠}) ⊆ 𝑋)
48	47	ad2antll 761	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ (𝑛 ∖ {𝑠}) ⊆ 𝑋)
49		inss1 3795	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝒫 𝑥 ∩ Fin) ⊆ 𝒫 𝑥
50	49	sseli 3564	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ 𝒫 𝑥)
51	50	elpwid 4118	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ⊆ 𝑥)
52	51	ad3antrrr 762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢) → 𝑡 ⊆ 𝑥)
53	52	ad2antlr 759	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑡 ⊆ 𝑥)
54		simprl 790	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑠 ∈ 𝑡)
55	53, 54	sseldd 3569	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑠 ∈ 𝑥)
56		elssuni 4403	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ 𝑥 → 𝑠 ⊆ ∪ 𝑥)
57	55, 56	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑠 ⊆ ∪ 𝑥)
58		fibas 20592	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (fi‘𝑥) ∈ TopBases
59		unitg 20582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((fi‘𝑥) ∈ TopBases → ∪ (topGen‘(fi‘𝑥)) = ∪ (fi‘𝑥))
60	58, 59	mp1i 13	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ (topGen‘(fi‘𝑥)) = ∪ (fi‘𝑥))
61		unieq 4380	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → ∪ 𝐽 = ∪ (topGen‘(fi‘𝑥)))
62	61	3ad2ant1 1075	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → ∪ 𝐽 = ∪ (topGen‘(fi‘𝑥)))
63	62	ad3antrrr 762	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝐽 = ∪ (topGen‘(fi‘𝑥)))
64		vex 3176	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ∈ V
65		fiuni 8217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ V → ∪ 𝑥 = ∪ (fi‘𝑥))
66	64, 65	mp1i 13	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑥 = ∪ (fi‘𝑥))
67	60, 63, 66	3eqtr4rd 2655	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑥 = ∪ 𝐽)
68		alexsubALT.1	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑋 = ∪ 𝐽
69	67, 68	syl6eqr 2662	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑥 = 𝑋)
70	57, 69	sseqtrd 3604	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑠 ⊆ 𝑋)
71	48, 70	unssd 3751	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠) ⊆ 𝑋)
72	42, 71	eqssd 3585	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑋 = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠))
73		unieq 4380	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = (𝑛 ∖ {𝑠}) → ∪ 𝑚 = ∪ (𝑛 ∖ {𝑠}))
74	73	uneq1d 3728	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝑛 ∖ {𝑠}) → (∪ 𝑚 ∪ 𝑠) = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠))
75	74	eqeq2d 2620	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝑛 ∖ {𝑠}) → (𝑋 = (∪ 𝑚 ∪ 𝑠) ↔ 𝑋 = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠)))
76	75	rspcev 3282	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠)) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠))
77	23, 72, 76	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠))
78	77	expr 641	. . . . . . . . . . . . 13 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ 𝑠 ∈ 𝑡) → ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠)))
79	78	expd 451	. . . . . . . . . . . 12 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ 𝑠 ∈ 𝑡) → (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) → (𝑋 = ∪ 𝑛 → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠))))
80	79	rexlimdv 3012	. . . . . . . . . . 11 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ 𝑠 ∈ 𝑡) → (∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛 → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠)))
81	80	ralimdva 2945	. . . . . . . . . 10 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (∀𝑠 ∈ 𝑡 ∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛 → ∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠)))
82		inss2 3796	. . . . . . . . . . . . . . 15 ⊢ (𝒫 𝑥 ∩ Fin) ⊆ Fin
83	82	sseli 3564	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ Fin)
84	83	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) → 𝑡 ∈ Fin)
85		unieq 4380	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝑓‘𝑠) → ∪ 𝑚 = ∪ (𝑓‘𝑠))
86	85	uneq1d 3728	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝑓‘𝑠) → (∪ 𝑚 ∪ 𝑠) = (∪ (𝑓‘𝑠) ∪ 𝑠))
87	86	eqeq2d 2620	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝑓‘𝑠) → (𝑋 = (∪ 𝑚 ∪ 𝑠) ↔ 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)))
88	87	ac6sfi 8089	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ Fin ∧ ∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠)) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)))
89	88	ex 449	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ Fin → (∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))))
90	84, 89	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) → (∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))))
91	90	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) → (∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))))
92	91	ad2antrl 760	. . . . . . . . . 10 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))))
93		ffvelrn 6265	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠 ∈ 𝑡) → (𝑓‘𝑠) ∈ (𝒫 𝑢 ∩ Fin))
94		elin 3758	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓‘𝑠) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((𝑓‘𝑠) ∈ 𝒫 𝑢 ∧ (𝑓‘𝑠) ∈ Fin))
95		elpwi 4117	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓‘𝑠) ∈ 𝒫 𝑢 → (𝑓‘𝑠) ⊆ 𝑢)
96	95	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓‘𝑠) ∈ 𝒫 𝑢 ∧ (𝑓‘𝑠) ∈ Fin) → (𝑓‘𝑠) ⊆ 𝑢)
97	94, 96	sylbi 206	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓‘𝑠) ∈ (𝒫 𝑢 ∩ Fin) → (𝑓‘𝑠) ⊆ 𝑢)
98	93, 97	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠 ∈ 𝑡) → (𝑓‘𝑠) ⊆ 𝑢)
99	98	ralrimiva 2949	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∀𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢)
100		iunss 4497	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢 ↔ ∀𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢)
101	99, 100	sylibr 223	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢)
102	101	ad2antrl 760	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢)
103		simplrr 797	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑤 ∈ 𝑢)
104	103	snssd 4281	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → {𝑤} ⊆ 𝑢)
105	102, 104	unssd 3751	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑢)
106		inss2 3796	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝒫 𝑢 ∩ Fin) ⊆ Fin
107	106, 93	sseldi 3566	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠 ∈ 𝑡) → (𝑓‘𝑠) ∈ Fin)
108	107	ralrimiva 2949	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∀𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
109		iunfi 8137	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ Fin ∧ ∀𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
110	84, 108, 109	syl2an 493	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin)) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
111	110	adantlr 747	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin)) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
112	111	adantlr 747	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢) ∧ 𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin)) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
113	112	ad2ant2lr 780	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
114		snfi 7923	. . . . . . . . . . . . . . . 16 ⊢ {𝑤} ∈ Fin
115		unfi 8112	. . . . . . . . . . . . . . . 16 ⊢ ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin ∧ {𝑤} ∈ Fin) → (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin)
116	113, 114, 115	sylancl 693	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin)
117	105, 116	jca 553	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin))
118		elin 3758	. . . . . . . . . . . . . . 15 ⊢ ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ∧ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin))
119	19	elpw2 4755	. . . . . . . . . . . . . . . 16 ⊢ ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ↔ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑢)
120	119	anbi1i 727	. . . . . . . . . . . . . . 15 ⊢ (((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ∧ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin) ↔ ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin))
121	118, 120	bitr2i 264	. . . . . . . . . . . . . 14 ⊢ (((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin) ↔ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin))
122	117, 121	sylib 207	. . . . . . . . . . . . 13 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin))
123		ralnex 2975	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠))
124	123	imbi2i 325	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) ↔ (𝑣 ∈ 𝑦 → ¬ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)))
125	124	albii 1737	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) ↔ ∀𝑦(𝑣 ∈ 𝑦 → ¬ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)))
126		alinexa 1759	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑦(𝑣 ∈ 𝑦 → ¬ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ↔ ¬ ∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)))
127	125, 126	bitr2i 264	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ ∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ↔ ∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)))
128		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑠 = 𝑧 → (𝑓‘𝑠) = (𝑓‘𝑧))
129	128	unieqd 4382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑠 = 𝑧 → ∪ (𝑓‘𝑠) = ∪ (𝑓‘𝑧))
130		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑠 = 𝑧 → 𝑠 = 𝑧)
131	129, 130	uneq12d 3730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑠 = 𝑧 → (∪ (𝑓‘𝑠) ∪ 𝑠) = (∪ (𝑓‘𝑧) ∪ 𝑧))
132	131	eqeq2d 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑠 = 𝑧 → (𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) ↔ 𝑋 = (∪ (𝑓‘𝑧) ∪ 𝑧)))
133	132	rspcv 3278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 ∈ 𝑡 → (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → 𝑋 = (∪ (𝑓‘𝑧) ∪ 𝑧)))
134		eleq2 2677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑋 = (∪ (𝑓‘𝑧) ∪ 𝑧) → (𝑣 ∈ 𝑋 ↔ 𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧)))
135	134	biimpd 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑋 = (∪ (𝑓‘𝑧) ∪ 𝑧) → (𝑣 ∈ 𝑋 → 𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧)))
136		elun 3715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧) ↔ (𝑣 ∈ ∪ (𝑓‘𝑧) ∨ 𝑣 ∈ 𝑧))
137		eluni 4375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑣 ∈ ∪ (𝑓‘𝑧) ↔ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)))
138	137	orbi1i 541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑣 ∈ ∪ (𝑓‘𝑧) ∨ 𝑣 ∈ 𝑧) ↔ (∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) ∨ 𝑣 ∈ 𝑧))
139		df-or 384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) ∨ 𝑣 ∈ 𝑧) ↔ (¬ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧))
140		alinexa 1759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧)) ↔ ¬ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)))
141	140	imbi1i 338	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧) ↔ (¬ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧))
142	139, 141	bitr4i 266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) ∨ 𝑣 ∈ 𝑧) ↔ (∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧))
143	136, 138, 142	3bitri 285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧) ↔ (∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧))
144		eleq2 2677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑦 = 𝑤 → (𝑣 ∈ 𝑦 ↔ 𝑣 ∈ 𝑤))
145		eleq1 2676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ (𝑓‘𝑠) ↔ 𝑤 ∈ (𝑓‘𝑠)))
146	145	notbid 307	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑦 = 𝑤 → (¬ 𝑦 ∈ (𝑓‘𝑠) ↔ ¬ 𝑤 ∈ (𝑓‘𝑠)))
147	146	ralbidv 2969	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑦 = 𝑤 → (∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠) ↔ ∀𝑠 ∈ 𝑡 ¬ 𝑤 ∈ (𝑓‘𝑠)))
148	144, 147	imbi12d 333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 = 𝑤 → ((𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) ↔ (𝑣 ∈ 𝑤 → ∀𝑠 ∈ 𝑡 ¬ 𝑤 ∈ (𝑓‘𝑠))))
149	148	spv 2248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → (𝑣 ∈ 𝑤 → ∀𝑠 ∈ 𝑡 ¬ 𝑤 ∈ (𝑓‘𝑠)))
150	128	eleq2d 2673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑠 = 𝑧 → (𝑤 ∈ (𝑓‘𝑠) ↔ 𝑤 ∈ (𝑓‘𝑧)))
151	150	notbid 307	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑠 = 𝑧 → (¬ 𝑤 ∈ (𝑓‘𝑠) ↔ ¬ 𝑤 ∈ (𝑓‘𝑧)))
152	151	rspcv 3278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑧 ∈ 𝑡 → (∀𝑠 ∈ 𝑡 ¬ 𝑤 ∈ (𝑓‘𝑠) → ¬ 𝑤 ∈ (𝑓‘𝑧)))
153	149, 152	syl9r 76	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 ∈ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → (𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧))))
154	153	alrimdv 1844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 ∈ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → ∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧))))
155	154	imim1d 80	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ 𝑡 → ((∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑧)))
156	143, 155	syl5bi 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 ∈ 𝑡 → (𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑧)))
157	156	a1dd 48	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 ∈ 𝑡 → (𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧) → (𝑤 = ∩ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑧))))
158	135, 157	syl9r 76	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 ∈ 𝑡 → (𝑋 = (∪ (𝑓‘𝑧) ∪ 𝑧) → (𝑣 ∈ 𝑋 → (𝑤 = ∩ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑧)))))
159	133, 158	syld 46	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 ∈ 𝑡 → (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (𝑣 ∈ 𝑋 → (𝑤 = ∩ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑧)))))
160	159	com14 94	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = ∩ 𝑡 → (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (𝑣 ∈ 𝑋 → (𝑧 ∈ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑧)))))
161	160	imp31 447	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (𝑧 ∈ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑧)))
162	161	com23 84	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → (𝑧 ∈ 𝑡 → 𝑣 ∈ 𝑧)))
163	162	ralrimdv 2951	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → ∀𝑧 ∈ 𝑡 𝑣 ∈ 𝑧))
164		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑣 ∈ V
165	164	elint2 4417	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 ∈ ∩ 𝑡 ↔ ∀𝑧 ∈ 𝑡 𝑣 ∈ 𝑧)
166	163, 165	syl6ibr 241	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ ∩ 𝑡))
167		eleq2 2677	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = ∩ 𝑡 → (𝑣 ∈ 𝑤 ↔ 𝑣 ∈ ∩ 𝑡))
168	167	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (𝑣 ∈ 𝑤 ↔ 𝑣 ∈ ∩ 𝑡))
169	166, 168	sylibrd 248	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑤))
170	127, 169	syl5bi 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (¬ ∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑤))
171	170	orrd 392	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ∨ 𝑣 ∈ 𝑤))
172	171	ex 449	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → (𝑣 ∈ 𝑋 → (∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ∨ 𝑣 ∈ 𝑤)))
173		orc 399	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) → (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤))
174	173	anim2i 591	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) → (𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
175	174	eximi 1752	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) → ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
176		equid 1926	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑤 = 𝑤
177		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑤 ∈ V
178		equequ1 1939	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑤 → (𝑦 = 𝑤 ↔ 𝑤 = 𝑤))
179	144, 178	anbi12d 743	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑤 → ((𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤) ↔ (𝑣 ∈ 𝑤 ∧ 𝑤 = 𝑤)))
180	177, 179	spcev 3273	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑣 ∈ 𝑤 ∧ 𝑤 = 𝑤) → ∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤))
181	176, 180	mpan2 703	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ 𝑤 → ∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤))
182		olc 398	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑤 → (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤))
183	182	anim2i 591	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤) → (𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
184	183	eximi 1752	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤) → ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
185	181, 184	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ 𝑤 → ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
186	175, 185	jaoi 393	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ∨ 𝑣 ∈ 𝑤) → ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
187		eluni 4375	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ ∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})))
188		elun 3715	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ (𝑦 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∨ 𝑦 ∈ {𝑤}))
189		eliun 4460	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ↔ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠))
190		velsn 4141	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ {𝑤} ↔ 𝑦 = 𝑤)
191	189, 190	orbi12i 542	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∨ 𝑦 ∈ {𝑤}) ↔ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤))
192	188, 191	bitri 263	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤))
193	192	anbi2i 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 ∈ 𝑦 ∧ 𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})) ↔ (𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
194	193	exbii 1764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})) ↔ ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
195	187, 194	bitr2i 264	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)) ↔ 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
196	186, 195	sylib 207	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ∨ 𝑣 ∈ 𝑤) → 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
197	172, 196	syl6 34	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → (𝑣 ∈ 𝑋 → 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})))
198	197	adantll 746	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → (𝑣 ∈ 𝑋 → 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})))
199	198	adantlr 747	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → (𝑣 ∈ 𝑋 → 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})))
200	199	adantlr 747	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → (𝑣 ∈ 𝑋 → 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})))
201	200	ad2ant2l 778	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (𝑣 ∈ 𝑋 → 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})))
202	201	ssrdv 3574	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑋 ⊆ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
203		elun 3715	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ (𝑣 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∨ 𝑣 ∈ {𝑤}))
204		eliun 4460	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ↔ ∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠))
205		velsn 4141	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ∈ {𝑤} ↔ 𝑣 = 𝑤)
206	204, 205	orbi12i 542	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∨ 𝑣 ∈ {𝑤}) ↔ (∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) ∨ 𝑣 = 𝑤))
207	203, 206	bitri 263	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ (∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) ∨ 𝑣 = 𝑤))
208		nfra1 2925	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑠∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)
209		nfv 1830	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑠 𝑣 ⊆ 𝑋
210		rsp 2913	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (𝑠 ∈ 𝑡 → 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)))
211		eqimss2 3621	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (∪ (𝑓‘𝑠) ∪ 𝑠) ⊆ 𝑋)
212		elssuni 4403	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ ∪ (𝑓‘𝑠))
213		ssun3 3740	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ⊆ ∪ (𝑓‘𝑠) → 𝑣 ⊆ (∪ (𝑓‘𝑠) ∪ 𝑠))
214	212, 213	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ (∪ (𝑓‘𝑠) ∪ 𝑠))
215		sstr 3576	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 ⊆ (∪ (𝑓‘𝑠) ∪ 𝑠) ∧ (∪ (𝑓‘𝑠) ∪ 𝑠) ⊆ 𝑋) → 𝑣 ⊆ 𝑋)
216	215	expcom 450	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((∪ (𝑓‘𝑠) ∪ 𝑠) ⊆ 𝑋 → (𝑣 ⊆ (∪ (𝑓‘𝑠) ∪ 𝑠) → 𝑣 ⊆ 𝑋))
217	211, 214, 216	syl2im 39	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ 𝑋))
218	210, 217	syl6 34	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (𝑠 ∈ 𝑡 → (𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ 𝑋)))
219	208, 209, 218	rexlimd 3008	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ 𝑋))
220	219	ad2antll 761	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ 𝑋))
221		elpwi 4117	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑢 ∈ 𝒫 (fi‘𝑥) → 𝑢 ⊆ (fi‘𝑥))
222	221	ad2antrl 760	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) → 𝑢 ⊆ (fi‘𝑥))
223	222	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑢 ⊆ (fi‘𝑥))
224	223, 103	sseldd 3569	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑤 ∈ (fi‘𝑥))
225		elssuni 4403	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ (fi‘𝑥) → 𝑤 ⊆ ∪ (fi‘𝑥))
226	224, 225	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑤 ⊆ ∪ (fi‘𝑥))
227	58, 59	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ (topGen‘(fi‘𝑥)) = ∪ (fi‘𝑥)
228	61, 227	syl6req 2661	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → ∪ (fi‘𝑥) = ∪ 𝐽)
229	228, 68	syl6eqr 2662	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → ∪ (fi‘𝑥) = 𝑋)
230	229	3ad2ant1 1075	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → ∪ (fi‘𝑥) = 𝑋)
231	230	ad3antrrr 762	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∪ (fi‘𝑥) = 𝑋)
232	226, 231	sseqtrd 3604	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑤 ⊆ 𝑋)
233		sseq1 3589	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = 𝑤 → (𝑣 ⊆ 𝑋 ↔ 𝑤 ⊆ 𝑋))
234	232, 233	syl5ibrcom 236	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (𝑣 = 𝑤 → 𝑣 ⊆ 𝑋))
235	220, 234	jaod 394	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ((∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) ∨ 𝑣 = 𝑤) → 𝑣 ⊆ 𝑋))
236	207, 235	syl5bi 231	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) → 𝑣 ⊆ 𝑋))
237	236	ralrimiv 2948	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∀𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})𝑣 ⊆ 𝑋)
238		unissb 4405	. . . . . . . . . . . . . . 15 ⊢ (∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑋 ↔ ∀𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})𝑣 ⊆ 𝑋)
239	237, 238	sylibr 223	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑋)
240	202, 239	eqssd 3585	. . . . . . . . . . . . 13 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑋 = ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
241		unieq 4380	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) → ∪ 𝑏 = ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
242	241	eqeq2d 2620	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) → (𝑋 = ∪ 𝑏 ↔ 𝑋 = ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})))
243	242	rspcev 3282	. . . . . . . . . . . . 13 ⊢ (((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏)
244	122, 240, 243	syl2anc 691	. . . . . . . . . . . 12 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏)
245	244	ex 449	. . . . . . . . . . 11 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏))
246	245	exlimdv 1848	. . . . . . . . . 10 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏))
247	81, 92, 246	3syld 58	. . . . . . . . 9 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (∀𝑠 ∈ 𝑡 ∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛 → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏))
248	4, 247	syl5bi 231	. . . . . . . 8 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (¬ ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛 → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏))
249		dfrex2 2979	. . . . . . . 8 ⊢ (∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏 ↔ ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)
250	248, 249	syl6ib 240	. . . . . . 7 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (¬ ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛 → ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))
251	250	con4d 113	. . . . . 6 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))
252	251	exp32 629	. . . . 5 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) → (𝑤 ∈ 𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))))
253	252	com24 93	. . . 4 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → (𝑤 ∈ 𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))))
254	253	exp32 629	. . 3 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (𝑢 ∈ 𝒫 (fi‘𝑥) → (𝑎 ⊆ 𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → (𝑤 ∈ 𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))))))
255	254	imp45 621	. 2 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑤 ∈ 𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)))
256	255	imp31 447	1 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  𝒫 cpw 4108  {csn 4125  ∪ cuni 4372  ∩ cint 4410  ∪ ciun 4455  ⟶wf 5800  ‘cfv 5804  Fincfn 7841  ficfi 8199  topGenctg 15921  TopBasesctb 20520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-fin 7845  df-fi 8200  df-topgen 15927  df-bases 20522

This theorem is referenced by:  alexsubALTlem4  21664