Theorem alexsubALTlem3 24057

Description: Lemma for alexsubALT 24059. 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 3073	. . . . . . . . . . 11 ⊢ (∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛 ↔ ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)
2	1	ralbii 3093	. . . . . . . . . 10 ⊢ (∀𝑠 ∈ 𝑡 ∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛 ↔ ∀𝑠 ∈ 𝑡 ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)
3		ralnex 3072	. . . . . . . . . 10 ⊢ (∀𝑠 ∈ 𝑡 ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛 ↔ ¬ ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)
4	2, 3	bitr2i 276	. . . . . . . . 9 ⊢ (¬ ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛 ↔ ∀𝑠 ∈ 𝑡 ∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛)
5		elin 3967	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ↔ (𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin))
6		elpwi 4607	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) → 𝑛 ⊆ (𝑢 ∪ {𝑠}))
7	6	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → 𝑛 ⊆ (𝑢 ∪ {𝑠}))
8		uncom 4158	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∪ {𝑠}) = ({𝑠} ∪ 𝑢)
9	7, 8	sseqtrdi 4024	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → 𝑛 ⊆ ({𝑠} ∪ 𝑢))
10		ssundif 4488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ⊆ ({𝑠} ∪ 𝑢) ↔ (𝑛 ∖ {𝑠}) ⊆ 𝑢)
11	9, 10	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → (𝑛 ∖ {𝑠}) ⊆ 𝑢)
12		diffi 9215	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ Fin → (𝑛 ∖ {𝑠}) ∈ Fin)
13	12	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → (𝑛 ∖ {𝑠}) ∈ Fin)
14	11, 13	jca 511	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
15	5, 14	sylbi 217	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
16	15	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
17	16	ad2antll 729	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
18		elin 3967	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
19		vex 3484	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑢 ∈ V
20	19	elpw2 5334	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ↔ (𝑛 ∖ {𝑠}) ⊆ 𝑢)
21	20	anbi1i 624	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin) ↔ ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
22	18, 21	bitr2i 276	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin) ↔ (𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin))
23	17, 22	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → (𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin))
24		simprrr 782	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑋 = ∪ 𝑛)
25		eldif 3961	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝑛 ∖ {𝑠}) ↔ (𝑥 ∈ 𝑛 ∧ ¬ 𝑥 ∈ {𝑠}))
26	25	simplbi2 500	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ 𝑛 → (¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})))
27		elun 4153	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) ↔ (𝑥 ∈ (𝑛 ∖ {𝑠}) ∨ 𝑥 ∈ {𝑠}))
28		orcom 871	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ (𝑥 ∈ (𝑛 ∖ {𝑠}) ∨ 𝑥 ∈ {𝑠}))
29	27, 28	bitr4i 278	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) ↔ (𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})))
30		df-or 849	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ (¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})))
31	29, 30	bitr2i 276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ 𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
32	26, 31	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝑛 → 𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
33	32	ssriv 3987	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑛 ⊆ ((𝑛 ∖ {𝑠}) ∪ {𝑠})
34		uniss 4915	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ⊆ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) → ∪ 𝑛 ⊆ ∪ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
35	33, 34	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑛 ⊆ ∪ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
36		uniun 4930	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) = (∪ (𝑛 ∖ {𝑠}) ∪ ∪ {𝑠})
37		unisnv 4927	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ {𝑠} = 𝑠
38	37	uneq2i 4165	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ (𝑛 ∖ {𝑠}) ∪ ∪ {𝑠}) = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠)
39	36, 38	eqtri 2765	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠)
40	35, 39	sseqtrdi 4024	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑛 ⊆ (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠))
41	24, 40	eqsstrd 4018	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑋 ⊆ (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠))
42		difss 4136	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∖ {𝑠}) ⊆ 𝑛
43	42	unissi 4916	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ (𝑛 ∖ {𝑠}) ⊆ ∪ 𝑛
44		sseq2 4010	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑋 = ∪ 𝑛 → (∪ (𝑛 ∖ {𝑠}) ⊆ 𝑋 ↔ ∪ (𝑛 ∖ {𝑠}) ⊆ ∪ 𝑛))
45	43, 44	mpbiri 258	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋 = ∪ 𝑛 → ∪ (𝑛 ∖ {𝑠}) ⊆ 𝑋)
46	45	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛) → ∪ (𝑛 ∖ {𝑠}) ⊆ 𝑋)
47	46	ad2antll 729	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ (𝑛 ∖ {𝑠}) ⊆ 𝑋)
48		elinel1 4201	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ 𝒫 𝑥)
49	48	elpwid 4609	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ⊆ 𝑥)
50	49	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢) → 𝑡 ⊆ 𝑥)
51	50	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑡 ⊆ 𝑥)
52		simprl 771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑠 ∈ 𝑡)
53	51, 52	sseldd 3984	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑠 ∈ 𝑥)
54		elssuni 4937	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ 𝑥 → 𝑠 ⊆ ∪ 𝑥)
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑠 ⊆ ∪ 𝑥)
56		fibas 22984	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (fi‘𝑥) ∈ TopBases
57		unitg 22974	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((fi‘𝑥) ∈ TopBases → ∪ (topGen‘(fi‘𝑥)) = ∪ (fi‘𝑥))
58	56, 57	mp1i 13	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ (topGen‘(fi‘𝑥)) = ∪ (fi‘𝑥))
59		unieq 4918	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → ∪ 𝐽 = ∪ (topGen‘(fi‘𝑥)))
60	59	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → ∪ 𝐽 = ∪ (topGen‘(fi‘𝑥)))
61	60	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝐽 = ∪ (topGen‘(fi‘𝑥)))
62		vex 3484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ∈ V
63		fiuni 9468	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ V → ∪ 𝑥 = ∪ (fi‘𝑥))
64	62, 63	mp1i 13	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑥 = ∪ (fi‘𝑥))
65	58, 61, 64	3eqtr4rd 2788	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑥 = ∪ 𝐽)
66		alexsubALT.1	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑋 = ∪ 𝐽
67	65, 66	eqtr4di 2795	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑥 = 𝑋)
68	55, 67	sseqtrd 4020	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑠 ⊆ 𝑋)
69	47, 68	unssd 4192	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠) ⊆ 𝑋)
70	41, 69	eqssd 4001	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑋 = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠))
71		unieq 4918	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝑛 ∖ {𝑠}) → ∪ 𝑚 = ∪ (𝑛 ∖ {𝑠}))
72	71	uneq1d 4167	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝑛 ∖ {𝑠}) → (∪ 𝑚 ∪ 𝑠) = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠))
73	72	rspceeqv 3645	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠)) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠))
74	23, 70, 73	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠))
75	74	expr 456	. . . . . . . . . . . . 13 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ 𝑠 ∈ 𝑡) → ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠)))
76	75	expd 415	. . . . . . . . . . . 12 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ 𝑠 ∈ 𝑡) → (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) → (𝑋 = ∪ 𝑛 → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠))))
77	76	rexlimdv 3153	. . . . . . . . . . 11 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ 𝑠 ∈ 𝑡) → (∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛 → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠)))
78	77	ralimdva 3167	. . . . . . . . . 10 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (∀𝑠 ∈ 𝑡 ∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛 → ∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠)))
79		elinel2 4202	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ Fin)
80	79	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) → 𝑡 ∈ Fin)
81		unieq 4918	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝑓‘𝑠) → ∪ 𝑚 = ∪ (𝑓‘𝑠))
82	81	uneq1d 4167	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝑓‘𝑠) → (∪ 𝑚 ∪ 𝑠) = (∪ (𝑓‘𝑠) ∪ 𝑠))
83	82	eqeq2d 2748	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝑓‘𝑠) → (𝑋 = (∪ 𝑚 ∪ 𝑠) ↔ 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)))
84	83	ac6sfi 9320	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ Fin ∧ ∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠)) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)))
85	84	ex 412	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ Fin → (∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))))
86	80, 85	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) → (∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))))
87	86	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) → (∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))))
88	87	ad2antrl 728	. . . . . . . . . 10 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))))
89		ffvelcdm 7101	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠 ∈ 𝑡) → (𝑓‘𝑠) ∈ (𝒫 𝑢 ∩ Fin))
90		elin 3967	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓‘𝑠) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((𝑓‘𝑠) ∈ 𝒫 𝑢 ∧ (𝑓‘𝑠) ∈ Fin))
91		elpwi 4607	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓‘𝑠) ∈ 𝒫 𝑢 → (𝑓‘𝑠) ⊆ 𝑢)
92	91	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓‘𝑠) ∈ 𝒫 𝑢 ∧ (𝑓‘𝑠) ∈ Fin) → (𝑓‘𝑠) ⊆ 𝑢)
93	90, 92	sylbi 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓‘𝑠) ∈ (𝒫 𝑢 ∩ Fin) → (𝑓‘𝑠) ⊆ 𝑢)
94	89, 93	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠 ∈ 𝑡) → (𝑓‘𝑠) ⊆ 𝑢)
95	94	ralrimiva 3146	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∀𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢)
96		iunss 5045	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢 ↔ ∀𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢)
97	95, 96	sylibr 234	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢)
98	97	ad2antrl 728	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢)
99		simplrr 778	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑤 ∈ 𝑢)
100	99	snssd 4809	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → {𝑤} ⊆ 𝑢)
101	98, 100	unssd 4192	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑢)
102	89	elin2d 4205	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠 ∈ 𝑡) → (𝑓‘𝑠) ∈ Fin)
103	102	ralrimiva 3146	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∀𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
104		iunfi 9383	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ Fin ∧ ∀𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
105	80, 103, 104	syl2an 596	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin)) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
106	105	ad4ant14 752	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢) ∧ 𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin)) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
107	106	ad2ant2lr 748	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
108		snfi 9083	. . . . . . . . . . . . . . . 16 ⊢ {𝑤} ∈ Fin
109		unfi 9211	. . . . . . . . . . . . . . . 16 ⊢ ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin ∧ {𝑤} ∈ Fin) → (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin)
110	107, 108, 109	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin)
111	101, 110	jca 511	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin))
112		elin 3967	. . . . . . . . . . . . . . 15 ⊢ ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ∧ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin))
113	19	elpw2 5334	. . . . . . . . . . . . . . . 16 ⊢ ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ↔ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑢)
114	113	anbi1i 624	. . . . . . . . . . . . . . 15 ⊢ (((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ∧ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin) ↔ ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin))
115	112, 114	bitr2i 276	. . . . . . . . . . . . . 14 ⊢ (((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin) ↔ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin))
116	111, 115	sylib 218	. . . . . . . . . . . . 13 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin))
117		ralnex 3072	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠))
118	117	imbi2i 336	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) ↔ (𝑣 ∈ 𝑦 → ¬ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)))
119	118	albii 1819	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) ↔ ∀𝑦(𝑣 ∈ 𝑦 → ¬ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)))
120		alinexa 1843	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦(𝑣 ∈ 𝑦 → ¬ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ↔ ¬ ∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)))
121	119, 120	bitr2i 276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ ∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ↔ ∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)))
122		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑠 = 𝑧 → (𝑓‘𝑠) = (𝑓‘𝑧))
123	122	unieqd 4920	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑠 = 𝑧 → ∪ (𝑓‘𝑠) = ∪ (𝑓‘𝑧))
124		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑠 = 𝑧 → 𝑠 = 𝑧)
125	123, 124	uneq12d 4169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑠 = 𝑧 → (∪ (𝑓‘𝑠) ∪ 𝑠) = (∪ (𝑓‘𝑧) ∪ 𝑧))
126	125	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑠 = 𝑧 → (𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) ↔ 𝑋 = (∪ (𝑓‘𝑧) ∪ 𝑧)))
127	126	rspcv 3618	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ 𝑡 → (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → 𝑋 = (∪ (𝑓‘𝑧) ∪ 𝑧)))
128		eleq2 2830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑋 = (∪ (𝑓‘𝑧) ∪ 𝑧) → (𝑣 ∈ 𝑋 ↔ 𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧)))
129	128	biimpd 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑋 = (∪ (𝑓‘𝑧) ∪ 𝑧) → (𝑣 ∈ 𝑋 → 𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧)))
130		elun 4153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧) ↔ (𝑣 ∈ ∪ (𝑓‘𝑧) ∨ 𝑣 ∈ 𝑧))
131		eluni 4910	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑣 ∈ ∪ (𝑓‘𝑧) ↔ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)))
132	131	orbi1i 914	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑣 ∈ ∪ (𝑓‘𝑧) ∨ 𝑣 ∈ 𝑧) ↔ (∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) ∨ 𝑣 ∈ 𝑧))
133		df-or 849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) ∨ 𝑣 ∈ 𝑧) ↔ (¬ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧))
134		alinexa 1843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧)) ↔ ¬ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)))
135	134	imbi1i 349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧) ↔ (¬ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧))
136	133, 135	bitr4i 278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) ∨ 𝑣 ∈ 𝑧) ↔ (∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧))
137	130, 132, 136	3bitri 297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧) ↔ (∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧))
138		eleq2 2830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 = 𝑤 → (𝑣 ∈ 𝑦 ↔ 𝑣 ∈ 𝑤))
139		eleq1w 2824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ (𝑓‘𝑠) ↔ 𝑤 ∈ (𝑓‘𝑠)))
140	139	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 = 𝑤 → (¬ 𝑦 ∈ (𝑓‘𝑠) ↔ ¬ 𝑤 ∈ (𝑓‘𝑠)))
141	140	ralbidv 3178	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 = 𝑤 → (∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠) ↔ ∀𝑠 ∈ 𝑡 ¬ 𝑤 ∈ (𝑓‘𝑠)))
142	138, 141	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 = 𝑤 → ((𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) ↔ (𝑣 ∈ 𝑤 → ∀𝑠 ∈ 𝑡 ¬ 𝑤 ∈ (𝑓‘𝑠))))
143	142	spvv 1996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → (𝑣 ∈ 𝑤 → ∀𝑠 ∈ 𝑡 ¬ 𝑤 ∈ (𝑓‘𝑠)))
144	122	eleq2d 2827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑠 = 𝑧 → (𝑤 ∈ (𝑓‘𝑠) ↔ 𝑤 ∈ (𝑓‘𝑧)))
145	144	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑠 = 𝑧 → (¬ 𝑤 ∈ (𝑓‘𝑠) ↔ ¬ 𝑤 ∈ (𝑓‘𝑧)))
146	145	rspcv 3618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 ∈ 𝑡 → (∀𝑠 ∈ 𝑡 ¬ 𝑤 ∈ (𝑓‘𝑠) → ¬ 𝑤 ∈ (𝑓‘𝑧)))
147	143, 146	syl9r 78	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → (𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧))))
148	147	alrimdv 1929	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 ∈ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → ∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧))))
149	148	imim1d 82	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 ∈ 𝑡 → ((∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑧)))
150	137, 149	biimtrid 242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 ∈ 𝑡 → (𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑧)))
151	150	a1dd 50	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 ∈ 𝑡 → (𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧) → (𝑤 = ∩ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑧))))
152	129, 151	syl9r 78	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ 𝑡 → (𝑋 = (∪ (𝑓‘𝑧) ∪ 𝑧) → (𝑣 ∈ 𝑋 → (𝑤 = ∩ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑧)))))
153	127, 152	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ 𝑡 → (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (𝑣 ∈ 𝑋 → (𝑤 = ∩ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑧)))))
154	153	com14 96	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = ∩ 𝑡 → (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (𝑣 ∈ 𝑋 → (𝑧 ∈ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑧)))))
155	154	imp31 417	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (𝑧 ∈ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑧)))
156	155	com23 86	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → (𝑧 ∈ 𝑡 → 𝑣 ∈ 𝑧)))
157	156	ralrimdv 3152	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → ∀𝑧 ∈ 𝑡 𝑣 ∈ 𝑧))
158		vex 3484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑣 ∈ V
159	158	elint2 4953	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ ∩ 𝑡 ↔ ∀𝑧 ∈ 𝑡 𝑣 ∈ 𝑧)
160	157, 159	imbitrrdi 252	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ ∩ 𝑡))
161		eleq2 2830	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = ∩ 𝑡 → (𝑣 ∈ 𝑤 ↔ 𝑣 ∈ ∩ 𝑡))
162	161	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (𝑣 ∈ 𝑤 ↔ 𝑣 ∈ ∩ 𝑡))
163	160, 162	sylibrd 259	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑤))
164	121, 163	biimtrid 242	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (¬ ∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑤))
165	164	orrd 864	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ∨ 𝑣 ∈ 𝑤))
166	165	ex 412	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → (𝑣 ∈ 𝑋 → (∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ∨ 𝑣 ∈ 𝑤)))
167		orc 868	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) → (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤))
168	167	anim2i 617	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) → (𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
169	168	eximi 1835	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) → ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
170		equid 2011	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑤 = 𝑤
171		vex 3484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑤 ∈ V
172		equequ1 2024	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑤 → (𝑦 = 𝑤 ↔ 𝑤 = 𝑤))
173	138, 172	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑤 → ((𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤) ↔ (𝑣 ∈ 𝑤 ∧ 𝑤 = 𝑤)))
174	171, 173	spcev 3606	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑣 ∈ 𝑤 ∧ 𝑤 = 𝑤) → ∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤))
175	170, 174	mpan2 691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ 𝑤 → ∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤))
176		olc 869	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑤 → (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤))
177	176	anim2i 617	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤) → (𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
178	177	eximi 1835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤) → ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
179	175, 178	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ 𝑤 → ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
180	169, 179	jaoi 858	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ∨ 𝑣 ∈ 𝑤) → ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
181		eluni 4910	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ ∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})))
182		elun 4153	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ (𝑦 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∨ 𝑦 ∈ {𝑤}))
183		eliun 4995	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ↔ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠))
184		velsn 4642	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ {𝑤} ↔ 𝑦 = 𝑤)
185	183, 184	orbi12i 915	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∨ 𝑦 ∈ {𝑤}) ↔ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤))
186	182, 185	bitri 275	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤))
187	186	anbi2i 623	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑣 ∈ 𝑦 ∧ 𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})) ↔ (𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
188	187	exbii 1848	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})) ↔ ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
189	181, 188	bitr2i 276	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)) ↔ 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
190	180, 189	sylib 218	. . . . . . . . . . . . . . . . . 18 ⊢ ((∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ∨ 𝑣 ∈ 𝑤) → 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
191	166, 190	syl6 35	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → (𝑣 ∈ 𝑋 → 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})))
192	191	ad5ant25 762	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → (𝑣 ∈ 𝑋 → 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})))
193	192	ad2ant2l 746	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (𝑣 ∈ 𝑋 → 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})))
194	193	ssrdv 3989	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑋 ⊆ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
195		elun 4153	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ (𝑣 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∨ 𝑣 ∈ {𝑤}))
196		eliun 4995	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ↔ ∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠))
197		velsn 4642	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ∈ {𝑤} ↔ 𝑣 = 𝑤)
198	196, 197	orbi12i 915	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∨ 𝑣 ∈ {𝑤}) ↔ (∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) ∨ 𝑣 = 𝑤))
199	195, 198	bitri 275	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ (∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) ∨ 𝑣 = 𝑤))
200		nfra1 3284	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑠∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)
201		nfv 1914	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑠 𝑣 ⊆ 𝑋
202		rsp 3247	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (𝑠 ∈ 𝑡 → 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)))
203		eqimss2 4043	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (∪ (𝑓‘𝑠) ∪ 𝑠) ⊆ 𝑋)
204		elssuni 4937	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ ∪ (𝑓‘𝑠))
205		ssun3 4180	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ⊆ ∪ (𝑓‘𝑠) → 𝑣 ⊆ (∪ (𝑓‘𝑠) ∪ 𝑠))
206	204, 205	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ (∪ (𝑓‘𝑠) ∪ 𝑠))
207		sstr 3992	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 ⊆ (∪ (𝑓‘𝑠) ∪ 𝑠) ∧ (∪ (𝑓‘𝑠) ∪ 𝑠) ⊆ 𝑋) → 𝑣 ⊆ 𝑋)
208	207	expcom 413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((∪ (𝑓‘𝑠) ∪ 𝑠) ⊆ 𝑋 → (𝑣 ⊆ (∪ (𝑓‘𝑠) ∪ 𝑠) → 𝑣 ⊆ 𝑋))
209	203, 206, 208	syl2im 40	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ 𝑋))
210	202, 209	syl6 35	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (𝑠 ∈ 𝑡 → (𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ 𝑋)))
211	200, 201, 210	rexlimd 3266	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ 𝑋))
212	211	ad2antll 729	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ 𝑋))
213		elpwi 4607	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑢 ∈ 𝒫 (fi‘𝑥) → 𝑢 ⊆ (fi‘𝑥))
214	213	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) → 𝑢 ⊆ (fi‘𝑥))
215	214	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑢 ⊆ (fi‘𝑥))
216	215, 99	sseldd 3984	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑤 ∈ (fi‘𝑥))
217		elssuni 4937	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ (fi‘𝑥) → 𝑤 ⊆ ∪ (fi‘𝑥))
218	216, 217	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑤 ⊆ ∪ (fi‘𝑥))
219	56, 57	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ (topGen‘(fi‘𝑥)) = ∪ (fi‘𝑥)
220	59, 219	eqtr2di 2794	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → ∪ (fi‘𝑥) = ∪ 𝐽)
221	220, 66	eqtr4di 2795	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → ∪ (fi‘𝑥) = 𝑋)
222	221	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → ∪ (fi‘𝑥) = 𝑋)
223	222	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∪ (fi‘𝑥) = 𝑋)
224	218, 223	sseqtrd 4020	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑤 ⊆ 𝑋)
225		sseq1 4009	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = 𝑤 → (𝑣 ⊆ 𝑋 ↔ 𝑤 ⊆ 𝑋))
226	224, 225	syl5ibrcom 247	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (𝑣 = 𝑤 → 𝑣 ⊆ 𝑋))
227	212, 226	jaod 860	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ((∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) ∨ 𝑣 = 𝑤) → 𝑣 ⊆ 𝑋))
228	199, 227	biimtrid 242	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) → 𝑣 ⊆ 𝑋))
229	228	ralrimiv 3145	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∀𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})𝑣 ⊆ 𝑋)
230		unissb 4939	. . . . . . . . . . . . . . 15 ⊢ (∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑋 ↔ ∀𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})𝑣 ⊆ 𝑋)
231	229, 230	sylibr 234	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑋)
232	194, 231	eqssd 4001	. . . . . . . . . . . . 13 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑋 = ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
233		unieq 4918	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) → ∪ 𝑏 = ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
234	233	rspceeqv 3645	. . . . . . . . . . . . 13 ⊢ (((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏)
235	116, 232, 234	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏)
236	235	ex 412	. . . . . . . . . . 11 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏))
237	236	exlimdv 1933	. . . . . . . . . 10 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏))
238	78, 88, 237	3syld 60	. . . . . . . . 9 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (∀𝑠 ∈ 𝑡 ∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛 → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏))
239	4, 238	biimtrid 242	. . . . . . . 8 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (¬ ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛 → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏))
240		dfrex2 3073	. . . . . . . 8 ⊢ (∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏 ↔ ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)
241	239, 240	imbitrdi 251	. . . . . . 7 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (¬ ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛 → ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))
242	241	con4d 115	. . . . . 6 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))
243	242	exp32 420	. . . . 5 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) → (𝑤 ∈ 𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))))
244	243	com24 95	. . . 4 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → (𝑤 ∈ 𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))))
245	244	exp32 420	. . 3 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (𝑢 ∈ 𝒫 (fi‘𝑥) → (𝑎 ⊆ 𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → (𝑤 ∈ 𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))))))
246	245	imp45 429	. 2 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑤 ∈ 𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)))
247	246	imp31 417	1 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2108  ∀wral 3061  ∃wrex 3070  Vcvv 3480   ∖ cdif 3948   ∪ cun 3949   ∩ cin 3950   ⊆ wss 3951  𝒫 cpw 4600  {csn 4626  ∪ cuni 4907  ∩ cint 4946  ∪ ciun 4991  ⟶wf 6557  ‘cfv 6561  Fincfn 8985  ficfi 9450  topGenctg 17482  TopBasesctb 22952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-om 7888  df-1o 8506  df-2o 8507  df-en 8986  df-fin 8989  df-fi 9451  df-topgen 17488  df-bases 22953

This theorem is referenced by:  alexsubALTlem4  24058