Theorem alexsubALTlem3 24167

Description: Lemma for alexsubALT 24169. 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 3092	. . . . . . . . . . 11 ⊢ (∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛 ↔ ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)
2	1	ralbii 3111	. . . . . . . . . 10 ⊢ (∀𝑠 ∈ 𝑡 ∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛 ↔ ∀𝑠 ∈ 𝑡 ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)
3		ralnex 3091	. . . . . . . . . 10 ⊢ (∀𝑠 ∈ 𝑡 ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛 ↔ ¬ ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)
4	2, 3	bitr2i 279	. . . . . . . . 9 ⊢ (¬ ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛 ↔ ∀𝑠 ∈ 𝑡 ∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛)
5		elin 3923	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ↔ (𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin))
6		elpwi 4565	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) → 𝑛 ⊆ (𝑢 ∪ {𝑠}))
7	6	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → 𝑛 ⊆ (𝑢 ∪ {𝑠}))
8		uncom 4114	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∪ {𝑠}) = ({𝑠} ∪ 𝑢)
9	7, 8	sseqtrdi 3979	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → 𝑛 ⊆ ({𝑠} ∪ 𝑢))
10		ssundif 4444	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ⊆ ({𝑠} ∪ 𝑢) ↔ (𝑛 ∖ {𝑠}) ⊆ 𝑢)
11	9, 10	sylib 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → (𝑛 ∖ {𝑠}) ⊆ 𝑢)
12		diffi 9147	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ Fin → (𝑛 ∖ {𝑠}) ∈ Fin)
13	12	adantl 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → (𝑛 ∖ {𝑠}) ∈ Fin)
14	11, 13	jca 520	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
15	5, 14	sylbi 220	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
16	15	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
17	16	ad2antll 741	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
18		elin 3923	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
19		vex 3461	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑢 ∈ V
20	19	elpw2 5295	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ↔ (𝑛 ∖ {𝑠}) ⊆ 𝑢)
21	20	anbi1i 635	. . . . . . . . . . . . . . . . 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 793	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑋 = ∪ 𝑛)
25		eldif 3917	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝑛 ∖ {𝑠}) ↔ (𝑥 ∈ 𝑛 ∧ ¬ 𝑥 ∈ {𝑠}))
26	25	simplbi2 505	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ 𝑛 → (¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})))
27		elun 4109	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) ↔ (𝑥 ∈ (𝑛 ∖ {𝑠}) ∨ 𝑥 ∈ {𝑠}))
28		orcom 883	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ (𝑥 ∈ (𝑛 ∖ {𝑠}) ∨ 𝑥 ∈ {𝑠}))
29	27, 28	bitr4i 281	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) ↔ (𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})))
30		df-or 861	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ (¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})))
31	29, 30	bitr2i 279	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ 𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
32	26, 31	sylib 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝑛 → 𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
33	32	ssriv 3943	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑛 ⊆ ((𝑛 ∖ {𝑠}) ∪ {𝑠})
34		uniss 4876	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ⊆ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) → ∪ 𝑛 ⊆ ∪ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
35	33, 34	mp1i 14	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑛 ⊆ ∪ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
36		uniun 4891	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) = (∪ (𝑛 ∖ {𝑠}) ∪ ∪ {𝑠})
37		unisnv 4888	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ {𝑠} = 𝑠
38	37	uneq2i 4121	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ (𝑛 ∖ {𝑠}) ∪ ∪ {𝑠}) = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠)
39	36, 38	eqtri 2788	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠)
40	35, 39	sseqtrdi 3979	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑛 ⊆ (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠))
41	24, 40	eqsstrd 3973	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑋 ⊆ (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠))
42		difss 4092	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∖ {𝑠}) ⊆ 𝑛
43	42	unissi 4877	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ (𝑛 ∖ {𝑠}) ⊆ ∪ 𝑛
44		sseq2 3965	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑋 = ∪ 𝑛 → (∪ (𝑛 ∖ {𝑠}) ⊆ 𝑋 ↔ ∪ (𝑛 ∖ {𝑠}) ⊆ ∪ 𝑛))
45	43, 44	mpbiri 261	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋 = ∪ 𝑛 → ∪ (𝑛 ∖ {𝑠}) ⊆ 𝑋)
46	45	adantl 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛) → ∪ (𝑛 ∖ {𝑠}) ⊆ 𝑋)
47	46	ad2antll 741	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ (𝑛 ∖ {𝑠}) ⊆ 𝑋)
48		elinel1 4156	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ 𝒫 𝑥)
49	48	elpwid 4567	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ⊆ 𝑥)
50	49	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢) → 𝑡 ⊆ 𝑥)
51	50	ad2antlr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑡 ⊆ 𝑥)
52		simprl 782	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑠 ∈ 𝑡)
53	51, 52	sseldd 3940	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑠 ∈ 𝑥)
54		elssuni 4900	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ 𝑥 → 𝑠 ⊆ ∪ 𝑥)
55	53, 54	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑠 ⊆ ∪ 𝑥)
56		fibas 23095	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (fi‘𝑥) ∈ TopBases
57		unitg 23085	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((fi‘𝑥) ∈ TopBases → ∪ (topGen‘(fi‘𝑥)) = ∪ (fi‘𝑥))
58	56, 57	mp1i 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ (topGen‘(fi‘𝑥)) = ∪ (fi‘𝑥))
59		unieq 4879	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → ∪ 𝐽 = ∪ (topGen‘(fi‘𝑥)))
60	59	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → ∪ 𝐽 = ∪ (topGen‘(fi‘𝑥)))
61	60	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝐽 = ∪ (topGen‘(fi‘𝑥)))
62		vex 3461	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ∈ V
63		fiuni 9376	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ V → ∪ 𝑥 = ∪ (fi‘𝑥))
64	62, 63	mp1i 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑥 = ∪ (fi‘𝑥))
65	58, 61, 64	3eqtr4rd 2811	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑥 = ∪ 𝐽)
66		alexsubALT.1	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑋 = ∪ 𝐽
67	65, 66	eqtr4di 2818	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑥 = 𝑋)
68	55, 67	sseqtrd 3975	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑠 ⊆ 𝑋)
69	47, 68	unssd 4147	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠) ⊆ 𝑋)
70	41, 69	eqssd 3956	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑋 = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠))
71		unieq 4879	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝑛 ∖ {𝑠}) → ∪ 𝑚 = ∪ (𝑛 ∖ {𝑠}))
72	71	uneq1d 4123	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝑛 ∖ {𝑠}) → (∪ 𝑚 ∪ 𝑠) = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠))
73	72	rspceeqv 3607	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠)) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠))
74	23, 70, 73	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠))
75	74	expr 461	. . . . . . . . . . . . 13 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ 𝑠 ∈ 𝑡) → ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠)))
76	75	expd 420	. . . . . . . . . . . 12 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ 𝑠 ∈ 𝑡) → (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) → (𝑋 = ∪ 𝑛 → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠))))
77	76	rexlimdv 3164	. . . . . . . . . . 11 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ 𝑠 ∈ 𝑡) → (∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛 → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠)))
78	77	ralimdva 3177	. . . . . . . . . 10 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (∀𝑠 ∈ 𝑡 ∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛 → ∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠)))
79		elinel2 4157	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ Fin)
80	79	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) → 𝑡 ∈ Fin)
81		unieq 4879	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝑓‘𝑠) → ∪ 𝑚 = ∪ (𝑓‘𝑠))
82	81	uneq1d 4123	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝑓‘𝑠) → (∪ 𝑚 ∪ 𝑠) = (∪ (𝑓‘𝑠) ∪ 𝑠))
83	82	eqeq2d 2776	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝑓‘𝑠) → (𝑋 = (∪ 𝑚 ∪ 𝑠) ↔ 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)))
84	83	ac6sfi 9232	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ Fin ∧ ∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠)) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)))
85	84	ex 417	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ Fin → (∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))))
86	80, 85	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) → (∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))))
87	86	adantr 485	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) → (∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))))
88	87	ad2antrl 740	. . . . . . . . . 10 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))))
89		ffvelcdm 7066	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠 ∈ 𝑡) → (𝑓‘𝑠) ∈ (𝒫 𝑢 ∩ Fin))
90		elin 3923	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓‘𝑠) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((𝑓‘𝑠) ∈ 𝒫 𝑢 ∧ (𝑓‘𝑠) ∈ Fin))
91		elpwi 4565	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓‘𝑠) ∈ 𝒫 𝑢 → (𝑓‘𝑠) ⊆ 𝑢)
92	91	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓‘𝑠) ∈ 𝒫 𝑢 ∧ (𝑓‘𝑠) ∈ Fin) → (𝑓‘𝑠) ⊆ 𝑢)
93	90, 92	sylbi 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓‘𝑠) ∈ (𝒫 𝑢 ∩ Fin) → (𝑓‘𝑠) ⊆ 𝑢)
94	89, 93	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠 ∈ 𝑡) → (𝑓‘𝑠) ⊆ 𝑢)
95	94	ralrimiva 3157	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∀𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢)
96		iunss 5005	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢 ↔ ∀𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢)
97	95, 96	sylibr 237	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢)
98	97	ad2antrl 740	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢)
99		simplrr 789	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑤 ∈ 𝑢)
100	99	snssd 4748	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → {𝑤} ⊆ 𝑢)
101	98, 100	unssd 4147	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑢)
102	89	elin2d 4160	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠 ∈ 𝑡) → (𝑓‘𝑠) ∈ Fin)
103	102	ralrimiva 3157	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∀𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
104		iunfi 9288	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ Fin ∧ ∀𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
105	80, 103, 104	syl2an 607	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin)) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
106	105	ad4ant14 764	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢) ∧ 𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin)) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
107	106	ad2ant2lr 760	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
108		snfi 9028	. . . . . . . . . . . . . . . 16 ⊢ {𝑤} ∈ Fin
109		unfi 9143	. . . . . . . . . . . . . . . 16 ⊢ ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin ∧ {𝑤} ∈ Fin) → (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin)
110	107, 108, 109	sylancl 597	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin)
111	101, 110	jca 520	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin))
112		elin 3923	. . . . . . . . . . . . . . 15 ⊢ ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ∧ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin))
113	19	elpw2 5295	. . . . . . . . . . . . . . . 16 ⊢ ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ↔ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑢)
114	113	anbi1i 635	. . . . . . . . . . . . . . 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 3091	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠))
118	117	imbi2i 339	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) ↔ (𝑣 ∈ 𝑦 → ¬ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)))
119	118	albii 1842	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) ↔ ∀𝑦(𝑣 ∈ 𝑦 → ¬ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)))
120		alinexa 1866	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦(𝑣 ∈ 𝑦 → ¬ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ↔ ¬ ∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)))
121	119, 120	bitr2i 279	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ ∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ↔ ∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)))
122		fveq2 6871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑠 = 𝑧 → (𝑓‘𝑠) = (𝑓‘𝑧))
123	122	unieqd 4881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑠 = 𝑧 → ∪ (𝑓‘𝑠) = ∪ (𝑓‘𝑧))
124		id 23	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑠 = 𝑧 → 𝑠 = 𝑧)
125	123, 124	uneq12d 4125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑠 = 𝑧 → (∪ (𝑓‘𝑠) ∪ 𝑠) = (∪ (𝑓‘𝑧) ∪ 𝑧))
126	125	eqeq2d 2776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑠 = 𝑧 → (𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) ↔ 𝑋 = (∪ (𝑓‘𝑧) ∪ 𝑧)))
127	126	rspcv 3580	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ 𝑡 → (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → 𝑋 = (∪ (𝑓‘𝑧) ∪ 𝑧)))
128		eleq2 2854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑋 = (∪ (𝑓‘𝑧) ∪ 𝑧) → (𝑣 ∈ 𝑋 ↔ 𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧)))
129	128	biimpd 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑋 = (∪ (𝑓‘𝑧) ∪ 𝑧) → (𝑣 ∈ 𝑋 → 𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧)))
130		elun 4109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧) ↔ (𝑣 ∈ ∪ (𝑓‘𝑧) ∨ 𝑣 ∈ 𝑧))
131		eluni 4871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑣 ∈ ∪ (𝑓‘𝑧) ↔ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)))
132	131	orbi1i 926	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑣 ∈ ∪ (𝑓‘𝑧) ∨ 𝑣 ∈ 𝑧) ↔ (∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) ∨ 𝑣 ∈ 𝑧))
133		df-or 861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) ∨ 𝑣 ∈ 𝑧) ↔ (¬ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧))
134		alinexa 1866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧)) ↔ ¬ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)))
135	134	imbi1i 352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧) ↔ (¬ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧))
136	133, 135	bitr4i 281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) ∨ 𝑣 ∈ 𝑧) ↔ (∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧))
137	130, 132, 136	3bitri 300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧) ↔ (∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧))
138		eleq2 2854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 = 𝑤 → (𝑣 ∈ 𝑦 ↔ 𝑣 ∈ 𝑤))
139		eleq1w 2848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ (𝑓‘𝑠) ↔ 𝑤 ∈ (𝑓‘𝑠)))
140	139	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 = 𝑤 → (¬ 𝑦 ∈ (𝑓‘𝑠) ↔ ¬ 𝑤 ∈ (𝑓‘𝑠)))
141	140	ralbidv 3188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 = 𝑤 → (∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠) ↔ ∀𝑠 ∈ 𝑡 ¬ 𝑤 ∈ (𝑓‘𝑠)))
142	138, 141	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 = 𝑤 → ((𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) ↔ (𝑣 ∈ 𝑤 → ∀𝑠 ∈ 𝑡 ¬ 𝑤 ∈ (𝑓‘𝑠))))
143	142	spvv 2011	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → (𝑣 ∈ 𝑤 → ∀𝑠 ∈ 𝑡 ¬ 𝑤 ∈ (𝑓‘𝑠)))
144	122	eleq2d 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑠 = 𝑧 → (𝑤 ∈ (𝑓‘𝑠) ↔ 𝑤 ∈ (𝑓‘𝑧)))
145	144	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑠 = 𝑧 → (¬ 𝑤 ∈ (𝑓‘𝑠) ↔ ¬ 𝑤 ∈ (𝑓‘𝑧)))
146	145	rspcv 3580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 ∈ 𝑡 → (∀𝑠 ∈ 𝑡 ¬ 𝑤 ∈ (𝑓‘𝑠) → ¬ 𝑤 ∈ (𝑓‘𝑧)))
147	143, 146	syl9r 79	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → (𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧))))
148	147	alrimdv 1952	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 422	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (𝑧 ∈ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑧)))
156	155	com23 87	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → (𝑧 ∈ 𝑡 → 𝑣 ∈ 𝑧)))
157	156	ralrimdv 3163	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → ∀𝑧 ∈ 𝑡 𝑣 ∈ 𝑧))
158		vex 3461	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑣 ∈ V
159	158	elint2 4915	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ ∩ 𝑡 ↔ ∀𝑧 ∈ 𝑡 𝑣 ∈ 𝑧)
160	157, 159	imbitrrdi 255	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ ∩ 𝑡))
161		eleq2 2854	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = ∩ 𝑡 → (𝑣 ∈ 𝑤 ↔ 𝑣 ∈ ∩ 𝑡))
162	161	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (𝑣 ∈ 𝑤 ↔ 𝑣 ∈ ∩ 𝑡))
163	160, 162	sylibrd 262	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑤))
164	121, 163	biimtrid 245	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (¬ ∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑤))
165	164	orrd 876	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ∨ 𝑣 ∈ 𝑤))
166	165	ex 417	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → (𝑣 ∈ 𝑋 → (∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ∨ 𝑣 ∈ 𝑤)))
167		orc 880	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) → (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤))
168	167	anim2i 628	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) → (𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
169	168	eximi 1858	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) → ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
170		equid 2035	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑤 = 𝑤
171		vex 3461	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑤 ∈ V
172		equequ1 2048	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑤 → (𝑦 = 𝑤 ↔ 𝑤 = 𝑤))
173	138, 172	anbi12d 643	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑤 → ((𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤) ↔ (𝑣 ∈ 𝑤 ∧ 𝑤 = 𝑤)))
174	171, 173	spcev 3568	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑣 ∈ 𝑤 ∧ 𝑤 = 𝑤) → ∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤))
175	170, 174	mpan2 703	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ 𝑤 → ∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤))
176		olc 881	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑤 → (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤))
177	176	anim2i 628	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤) → (𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
178	177	eximi 1858	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤) → ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
179	175, 178	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ 𝑤 → ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
180	169, 179	jaoi 870	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ∨ 𝑣 ∈ 𝑤) → ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
181		eluni 4871	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ ∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})))
182		elun 4109	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ (𝑦 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∨ 𝑦 ∈ {𝑤}))
183		eliun 4956	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ↔ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠))
184		velsn 4601	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ {𝑤} ↔ 𝑦 = 𝑤)
185	183, 184	orbi12i 927	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∨ 𝑦 ∈ {𝑤}) ↔ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤))
186	182, 185	bitri 278	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤))
187	186	anbi2i 634	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑣 ∈ 𝑦 ∧ 𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})) ↔ (𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
188	187	exbii 1871	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})) ↔ ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
189	181, 188	bitr2i 279	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)) ↔ 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
190	180, 189	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ ((∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ∨ 𝑣 ∈ 𝑤) → 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
191	166, 190	syl6 36	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → (𝑣 ∈ 𝑋 → 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})))
192	191	ad5ant25 773	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → (𝑣 ∈ 𝑋 → 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})))
193	192	ad2ant2l 758	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (𝑣 ∈ 𝑋 → 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})))
194	193	ssrdv 3945	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑋 ⊆ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
195		elun 4109	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ (𝑣 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∨ 𝑣 ∈ {𝑤}))
196		eliun 4956	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ↔ ∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠))
197		velsn 4601	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ∈ {𝑤} ↔ 𝑣 = 𝑤)
198	196, 197	orbi12i 927	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∨ 𝑣 ∈ {𝑤}) ↔ (∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) ∨ 𝑣 = 𝑤))
199	195, 198	bitri 278	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ (∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) ∨ 𝑣 = 𝑤))
200		nfra1 3289	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑠∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)
201		nfv 1937	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑠 𝑣 ⊆ 𝑋
202		rsp 3253	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (𝑠 ∈ 𝑡 → 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)))
203		eqimss2 3998	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (∪ (𝑓‘𝑠) ∪ 𝑠) ⊆ 𝑋)
204		elssuni 4900	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ ∪ (𝑓‘𝑠))
205		ssun3 4135	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ⊆ ∪ (𝑓‘𝑠) → 𝑣 ⊆ (∪ (𝑓‘𝑠) ∪ 𝑠))
206	204, 205	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ (∪ (𝑓‘𝑠) ∪ 𝑠))
207		sstr 3947	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 ⊆ (∪ (𝑓‘𝑠) ∪ 𝑠) ∧ (∪ (𝑓‘𝑠) ∪ 𝑠) ⊆ 𝑋) → 𝑣 ⊆ 𝑋)
208	207	expcom 418	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((∪ (𝑓‘𝑠) ∪ 𝑠) ⊆ 𝑋 → (𝑣 ⊆ (∪ (𝑓‘𝑠) ∪ 𝑠) → 𝑣 ⊆ 𝑋))
209	203, 206, 208	syl2im 41	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ 𝑋))
210	202, 209	syl6 36	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (𝑠 ∈ 𝑡 → (𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ 𝑋)))
211	200, 201, 210	rexlimd 3272	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ 𝑋))
212	211	ad2antll 741	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ 𝑋))
213		elpwi 4565	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑢 ∈ 𝒫 (fi‘𝑥) → 𝑢 ⊆ (fi‘𝑥))
214	213	ad2antrl 740	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) → 𝑢 ⊆ (fi‘𝑥))
215	214	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑢 ⊆ (fi‘𝑥))
216	215, 99	sseldd 3940	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑤 ∈ (fi‘𝑥))
217		elssuni 4900	. . . . . . . . . . . . . . . . . . . . 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 2817	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → ∪ (fi‘𝑥) = ∪ 𝐽)
221	220, 66	eqtr4di 2818	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → ∪ (fi‘𝑥) = 𝑋)
222	221	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → ∪ (fi‘𝑥) = 𝑋)
223	222	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∪ (fi‘𝑥) = 𝑋)
224	218, 223	sseqtrd 3975	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑤 ⊆ 𝑋)
225		sseq1 3964	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = 𝑤 → (𝑣 ⊆ 𝑋 ↔ 𝑤 ⊆ 𝑋))
226	224, 225	syl5ibrcom 250	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (𝑣 = 𝑤 → 𝑣 ⊆ 𝑋))
227	212, 226	jaod 872	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ((∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) ∨ 𝑣 = 𝑤) → 𝑣 ⊆ 𝑋))
228	199, 227	biimtrid 245	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) → 𝑣 ⊆ 𝑋))
229	228	ralrimiv 3156	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∀𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})𝑣 ⊆ 𝑋)
230		unissb 4902	. . . . . . . . . . . . . . 15 ⊢ (∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑋 ↔ ∀𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})𝑣 ⊆ 𝑋)
231	229, 230	sylibr 237	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑋)
232	194, 231	eqssd 3956	. . . . . . . . . . . . 13 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑋 = ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
233		unieq 4879	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) → ∪ 𝑏 = ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
234	233	rspceeqv 3607	. . . . . . . . . . . . 13 ⊢ (((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏)
235	116, 232, 234	syl2anc 595	. . . . . . . . . . . 12 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏)
236	235	ex 417	. . . . . . . . . . 11 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏))
237	236	exlimdv 1956	. . . . . . . . . 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 3092	. . . . . . . 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 425	. . . . 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 425	. . 3 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (𝑢 ∈ 𝒫 (fi‘𝑥) → (𝑎 ⊆ 𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → (𝑤 ∈ 𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))))))
246	245	imp45 434	. 2 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑤 ∈ 𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)))
247	246	imp31 422	1 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∧ w3a 1101  ∀wal 1561   = wceq 1563  ∃wex 1802   ∈ wcel 2145  ∀wral 3079  ∃wrex 3089  Vcvv 3457   ∖ cdif 3904   ∪ cun 3905   ∩ cin 3906   ⊆ wss 3907  𝒫 cpw 4558  {csn 4585  ∪ cuni 4868  ∩ cint 4908  ∪ ciun 4952  ⟶wf 6521  ‘cfv 6525  Fincfn 8931  ficfi 9358  topGenctg 17480  TopBasesctb 23063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-int 4909  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-om 7851  df-1o 8441  df-2o 8442  df-en 8932  df-fin 8935  df-fi 9359  df-topgen 17486  df-bases 23064

This theorem is referenced by:  alexsubALTlem4  24168