Theorem alexsubALTlem3 23400

Description: Lemma for alexsubALT 23402. 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 3076	. . . . . . . . . . 11 ⊢ (∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛 ↔ ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)
2	1	ralbii 3096	. . . . . . . . . 10 ⊢ (∀𝑠 ∈ 𝑡 ∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛 ↔ ∀𝑠 ∈ 𝑡 ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)
3		ralnex 3075	. . . . . . . . . 10 ⊢ (∀𝑠 ∈ 𝑡 ¬ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛 ↔ ¬ ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)
4	2, 3	bitr2i 275	. . . . . . . . 9 ⊢ (¬ ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛 ↔ ∀𝑠 ∈ 𝑡 ∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛)
5		elin 3926	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ↔ (𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin))
6		elpwi 4567	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) → 𝑛 ⊆ (𝑢 ∪ {𝑠}))
7	6	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → 𝑛 ⊆ (𝑢 ∪ {𝑠}))
8		uncom 4113	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∪ {𝑠}) = ({𝑠} ∪ 𝑢)
9	7, 8	sseqtrdi 3994	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → 𝑛 ⊆ ({𝑠} ∪ 𝑢))
10		ssundif 4445	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ⊆ ({𝑠} ∪ 𝑢) ↔ (𝑛 ∖ {𝑠}) ⊆ 𝑢)
11	9, 10	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → (𝑛 ∖ {𝑠}) ⊆ 𝑢)
12		diffi 9123	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ Fin → (𝑛 ∖ {𝑠}) ∈ Fin)
13	12	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → (𝑛 ∖ {𝑠}) ∈ Fin)
14	11, 13	jca 512	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ 𝒫 (𝑢 ∪ {𝑠}) ∧ 𝑛 ∈ Fin) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
15	5, 14	sylbi 216	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
16	15	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
17	16	ad2antll 727	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
18		elin 3926	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
19		vex 3449	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑢 ∈ V
20	19	elpw2 5302	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ↔ (𝑛 ∖ {𝑠}) ⊆ 𝑢)
21	20	anbi1i 624	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∖ {𝑠}) ∈ 𝒫 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin) ↔ ((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin))
22	18, 21	bitr2i 275	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∖ {𝑠}) ⊆ 𝑢 ∧ (𝑛 ∖ {𝑠}) ∈ Fin) ↔ (𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin))
23	17, 22	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → (𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin))
24		simprrr 780	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑋 = ∪ 𝑛)
25		eldif 3920	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝑛 ∖ {𝑠}) ↔ (𝑥 ∈ 𝑛 ∧ ¬ 𝑥 ∈ {𝑠}))
26	25	simplbi2 501	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ 𝑛 → (¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})))
27		elun 4108	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) ↔ (𝑥 ∈ (𝑛 ∖ {𝑠}) ∨ 𝑥 ∈ {𝑠}))
28		orcom 868	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ (𝑥 ∈ (𝑛 ∖ {𝑠}) ∨ 𝑥 ∈ {𝑠}))
29	27, 28	bitr4i 277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) ↔ (𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})))
30		df-or 846	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ {𝑠} ∨ 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ (¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})))
31	29, 30	bitr2i 275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ 𝑥 ∈ {𝑠} → 𝑥 ∈ (𝑛 ∖ {𝑠})) ↔ 𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
32	26, 31	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝑛 → 𝑥 ∈ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
33	32	ssriv 3948	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑛 ⊆ ((𝑛 ∖ {𝑠}) ∪ {𝑠})
34		uniss 4873	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ⊆ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) → ∪ 𝑛 ⊆ ∪ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
35	33, 34	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑛 ⊆ ∪ ((𝑛 ∖ {𝑠}) ∪ {𝑠}))
36		uniun 4891	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) = (∪ (𝑛 ∖ {𝑠}) ∪ ∪ {𝑠})
37		unisnv 4888	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ {𝑠} = 𝑠
38	37	uneq2i 4120	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ (𝑛 ∖ {𝑠}) ∪ ∪ {𝑠}) = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠)
39	36, 38	eqtri 2764	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ ((𝑛 ∖ {𝑠}) ∪ {𝑠}) = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠)
40	35, 39	sseqtrdi 3994	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑛 ⊆ (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠))
41	24, 40	eqsstrd 3982	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑋 ⊆ (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠))
42		difss 4091	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∖ {𝑠}) ⊆ 𝑛
43	42	unissi 4874	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ (𝑛 ∖ {𝑠}) ⊆ ∪ 𝑛
44		sseq2 3970	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑋 = ∪ 𝑛 → (∪ (𝑛 ∖ {𝑠}) ⊆ 𝑋 ↔ ∪ (𝑛 ∖ {𝑠}) ⊆ ∪ 𝑛))
45	43, 44	mpbiri 257	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋 = ∪ 𝑛 → ∪ (𝑛 ∖ {𝑠}) ⊆ 𝑋)
46	45	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛) → ∪ (𝑛 ∖ {𝑠}) ⊆ 𝑋)
47	46	ad2antll 727	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ (𝑛 ∖ {𝑠}) ⊆ 𝑋)
48		elinel1 4155	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ 𝒫 𝑥)
49	48	elpwid 4569	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ⊆ 𝑥)
50	49	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢) → 𝑡 ⊆ 𝑥)
51	50	ad2antlr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑡 ⊆ 𝑥)
52		simprl 769	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑠 ∈ 𝑡)
53	51, 52	sseldd 3945	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑠 ∈ 𝑥)
54		elssuni 4898	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ 𝑥 → 𝑠 ⊆ ∪ 𝑥)
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑠 ⊆ ∪ 𝑥)
56		fibas 22327	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (fi‘𝑥) ∈ TopBases
57		unitg 22317	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((fi‘𝑥) ∈ TopBases → ∪ (topGen‘(fi‘𝑥)) = ∪ (fi‘𝑥))
58	56, 57	mp1i 13	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ (topGen‘(fi‘𝑥)) = ∪ (fi‘𝑥))
59		unieq 4876	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → ∪ 𝐽 = ∪ (topGen‘(fi‘𝑥)))
60	59	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → ∪ 𝐽 = ∪ (topGen‘(fi‘𝑥)))
61	60	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝐽 = ∪ (topGen‘(fi‘𝑥)))
62		vex 3449	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ∈ V
63		fiuni 9364	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ V → ∪ 𝑥 = ∪ (fi‘𝑥))
64	62, 63	mp1i 13	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑥 = ∪ (fi‘𝑥))
65	58, 61, 64	3eqtr4rd 2787	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑥 = ∪ 𝐽)
66		alexsubALT.1	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑋 = ∪ 𝐽
67	65, 66	eqtr4di 2794	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∪ 𝑥 = 𝑋)
68	55, 67	sseqtrd 3984	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑠 ⊆ 𝑋)
69	47, 68	unssd 4146	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠) ⊆ 𝑋)
70	41, 69	eqssd 3961	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → 𝑋 = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠))
71		unieq 4876	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝑛 ∖ {𝑠}) → ∪ 𝑚 = ∪ (𝑛 ∖ {𝑠}))
72	71	uneq1d 4122	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝑛 ∖ {𝑠}) → (∪ 𝑚 ∪ 𝑠) = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠))
73	72	rspceeqv 3595	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∖ {𝑠}) ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = (∪ (𝑛 ∖ {𝑠}) ∪ 𝑠)) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠))
74	23, 70, 73	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑠 ∈ 𝑡 ∧ (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛))) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠))
75	74	expr 457	. . . . . . . . . . . . 13 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ 𝑠 ∈ 𝑡) → ((𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ∧ 𝑋 = ∪ 𝑛) → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠)))
76	75	expd 416	. . . . . . . . . . . 12 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ 𝑠 ∈ 𝑡) → (𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) → (𝑋 = ∪ 𝑛 → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠))))
77	76	rexlimdv 3150	. . . . . . . . . . 11 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ 𝑠 ∈ 𝑡) → (∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛 → ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠)))
78	77	ralimdva 3164	. . . . . . . . . 10 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (∀𝑠 ∈ 𝑡 ∃𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin)𝑋 = ∪ 𝑛 → ∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠)))
79		elinel2 4156	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ Fin)
80	79	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) → 𝑡 ∈ Fin)
81		unieq 4876	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝑓‘𝑠) → ∪ 𝑚 = ∪ (𝑓‘𝑠))
82	81	uneq1d 4122	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝑓‘𝑠) → (∪ 𝑚 ∪ 𝑠) = (∪ (𝑓‘𝑠) ∪ 𝑠))
83	82	eqeq2d 2747	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝑓‘𝑠) → (𝑋 = (∪ 𝑚 ∪ 𝑠) ↔ 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)))
84	83	ac6sfi 9231	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ Fin ∧ ∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠)) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)))
85	84	ex 413	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ Fin → (∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))))
86	80, 85	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) → (∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))))
87	86	adantr 481	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) → (∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))))
88	87	ad2antrl 726	. . . . . . . . . 10 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (∀𝑠 ∈ 𝑡 ∃𝑚 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = (∪ 𝑚 ∪ 𝑠) → ∃𝑓(𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))))
89		ffvelcdm 7032	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠 ∈ 𝑡) → (𝑓‘𝑠) ∈ (𝒫 𝑢 ∩ Fin))
90		elin 3926	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓‘𝑠) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((𝑓‘𝑠) ∈ 𝒫 𝑢 ∧ (𝑓‘𝑠) ∈ Fin))
91		elpwi 4567	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓‘𝑠) ∈ 𝒫 𝑢 → (𝑓‘𝑠) ⊆ 𝑢)
92	91	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓‘𝑠) ∈ 𝒫 𝑢 ∧ (𝑓‘𝑠) ∈ Fin) → (𝑓‘𝑠) ⊆ 𝑢)
93	90, 92	sylbi 216	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓‘𝑠) ∈ (𝒫 𝑢 ∩ Fin) → (𝑓‘𝑠) ⊆ 𝑢)
94	89, 93	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠 ∈ 𝑡) → (𝑓‘𝑠) ⊆ 𝑢)
95	94	ralrimiva 3143	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∀𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢)
96		iunss 5005	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢 ↔ ∀𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢)
97	95, 96	sylibr 233	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢)
98	97	ad2antrl 726	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ⊆ 𝑢)
99		simplrr 776	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑤 ∈ 𝑢)
100	99	snssd 4769	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → {𝑤} ⊆ 𝑢)
101	98, 100	unssd 4146	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑢)
102	89	elin2d 4159	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ 𝑠 ∈ 𝑡) → (𝑓‘𝑠) ∈ Fin)
103	102	ralrimiva 3143	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) → ∀𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
104		iunfi 9284	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ Fin ∧ ∀𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
105	80, 103, 104	syl2an 596	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin)) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
106	105	ad4ant14 750	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢) ∧ 𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin)) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
107	106	ad2ant2lr 746	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin)
108		snfi 8988	. . . . . . . . . . . . . . . 16 ⊢ {𝑤} ∈ Fin
109		unfi 9116	. . . . . . . . . . . . . . . 16 ⊢ ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∈ Fin ∧ {𝑤} ∈ Fin) → (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin)
110	107, 108, 109	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin)
111	101, 110	jca 512	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin))
112		elin 3926	. . . . . . . . . . . . . . 15 ⊢ ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin) ↔ ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ∧ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin))
113	19	elpw2 5302	. . . . . . . . . . . . . . . 16 ⊢ ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ↔ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑢)
114	113	anbi1i 624	. . . . . . . . . . . . . . 15 ⊢ (((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ 𝒫 𝑢 ∧ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin) ↔ ((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin))
115	112, 114	bitr2i 275	. . . . . . . . . . . . . 14 ⊢ (((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑢 ∧ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ Fin) ↔ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin))
116	111, 115	sylib 217	. . . . . . . . . . . . 13 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin))
117		ralnex 3075	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠))
118	117	imbi2i 335	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) ↔ (𝑣 ∈ 𝑦 → ¬ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)))
119	118	albii 1821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) ↔ ∀𝑦(𝑣 ∈ 𝑦 → ¬ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)))
120		alinexa 1845	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦(𝑣 ∈ 𝑦 → ¬ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ↔ ¬ ∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)))
121	119, 120	bitr2i 275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ ∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ↔ ∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)))
122		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑠 = 𝑧 → (𝑓‘𝑠) = (𝑓‘𝑧))
123	122	unieqd 4879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑠 = 𝑧 → ∪ (𝑓‘𝑠) = ∪ (𝑓‘𝑧))
124		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑠 = 𝑧 → 𝑠 = 𝑧)
125	123, 124	uneq12d 4124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑠 = 𝑧 → (∪ (𝑓‘𝑠) ∪ 𝑠) = (∪ (𝑓‘𝑧) ∪ 𝑧))
126	125	eqeq2d 2747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑠 = 𝑧 → (𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) ↔ 𝑋 = (∪ (𝑓‘𝑧) ∪ 𝑧)))
127	126	rspcv 3577	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ 𝑡 → (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → 𝑋 = (∪ (𝑓‘𝑧) ∪ 𝑧)))
128		eleq2 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑋 = (∪ (𝑓‘𝑧) ∪ 𝑧) → (𝑣 ∈ 𝑋 ↔ 𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧)))
129	128	biimpd 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑋 = (∪ (𝑓‘𝑧) ∪ 𝑧) → (𝑣 ∈ 𝑋 → 𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧)))
130		elun 4108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧) ↔ (𝑣 ∈ ∪ (𝑓‘𝑧) ∨ 𝑣 ∈ 𝑧))
131		eluni 4868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑣 ∈ ∪ (𝑓‘𝑧) ↔ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)))
132	131	orbi1i 912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑣 ∈ ∪ (𝑓‘𝑧) ∨ 𝑣 ∈ 𝑧) ↔ (∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) ∨ 𝑣 ∈ 𝑧))
133		df-or 846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) ∨ 𝑣 ∈ 𝑧) ↔ (¬ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧))
134		alinexa 1845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧)) ↔ ¬ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)))
135	134	imbi1i 349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧) ↔ (¬ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧))
136	133, 135	bitr4i 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑓‘𝑧)) ∨ 𝑣 ∈ 𝑧) ↔ (∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧))
137	130, 132, 136	3bitri 296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑣 ∈ (∪ (𝑓‘𝑧) ∪ 𝑧) ↔ (∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧))
138		eleq2 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 = 𝑤 → (𝑣 ∈ 𝑦 ↔ 𝑣 ∈ 𝑤))
139		eleq1w 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ (𝑓‘𝑠) ↔ 𝑤 ∈ (𝑓‘𝑠)))
140	139	notbid 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 = 𝑤 → (¬ 𝑦 ∈ (𝑓‘𝑠) ↔ ¬ 𝑤 ∈ (𝑓‘𝑠)))
141	140	ralbidv 3174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 = 𝑤 → (∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠) ↔ ∀𝑠 ∈ 𝑡 ¬ 𝑤 ∈ (𝑓‘𝑠)))
142	138, 141	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 = 𝑤 → ((𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) ↔ (𝑣 ∈ 𝑤 → ∀𝑠 ∈ 𝑡 ¬ 𝑤 ∈ (𝑓‘𝑠))))
143	142	spvv 2000	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → (𝑣 ∈ 𝑤 → ∀𝑠 ∈ 𝑡 ¬ 𝑤 ∈ (𝑓‘𝑠)))
144	122	eleq2d 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑠 = 𝑧 → (𝑤 ∈ (𝑓‘𝑠) ↔ 𝑤 ∈ (𝑓‘𝑧)))
145	144	notbid 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑠 = 𝑧 → (¬ 𝑤 ∈ (𝑓‘𝑠) ↔ ¬ 𝑤 ∈ (𝑓‘𝑧)))
146	145	rspcv 3577	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 ∈ 𝑡 → (∀𝑠 ∈ 𝑡 ¬ 𝑤 ∈ (𝑓‘𝑠) → ¬ 𝑤 ∈ (𝑓‘𝑧)))
147	143, 146	syl9r 78	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → (𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧))))
148	147	alrimdv 1932	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 ∈ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → ∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧))))
149	148	imim1d 82	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 ∈ 𝑡 → ((∀𝑤(𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ (𝑓‘𝑧)) → 𝑣 ∈ 𝑧) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑧)))
150	137, 149	biimtrid 241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 418	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (𝑧 ∈ 𝑡 → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑧)))
156	155	com23 86	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → (𝑧 ∈ 𝑡 → 𝑣 ∈ 𝑧)))
157	156	ralrimdv 3149	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → ∀𝑧 ∈ 𝑡 𝑣 ∈ 𝑧))
158		vex 3449	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑣 ∈ V
159	158	elint2 4914	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ ∩ 𝑡 ↔ ∀𝑧 ∈ 𝑡 𝑣 ∈ 𝑧)
160	157, 159	syl6ibr 251	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ ∩ 𝑡))
161		eleq2 2826	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = ∩ 𝑡 → (𝑣 ∈ 𝑤 ↔ 𝑣 ∈ ∩ 𝑡))
162	161	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (𝑣 ∈ 𝑤 ↔ 𝑣 ∈ ∩ 𝑡))
163	160, 162	sylibrd 258	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∀𝑦(𝑣 ∈ 𝑦 → ∀𝑠 ∈ 𝑡 ¬ 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑤))
164	121, 163	biimtrid 241	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (¬ ∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) → 𝑣 ∈ 𝑤))
165	164	orrd 861	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) ∧ 𝑣 ∈ 𝑋) → (∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ∨ 𝑣 ∈ 𝑤))
166	165	ex 413	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → (𝑣 ∈ 𝑋 → (∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ∨ 𝑣 ∈ 𝑤)))
167		orc 865	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) → (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤))
168	167	anim2i 617	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) → (𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
169	168	eximi 1837	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) → ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
170		equid 2015	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑤 = 𝑤
171		vex 3449	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑤 ∈ V
172		equequ1 2028	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑤 → (𝑦 = 𝑤 ↔ 𝑤 = 𝑤))
173	138, 172	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑤 → ((𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤) ↔ (𝑣 ∈ 𝑤 ∧ 𝑤 = 𝑤)))
174	171, 173	spcev 3565	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑣 ∈ 𝑤 ∧ 𝑤 = 𝑤) → ∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤))
175	170, 174	mpan2 689	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ 𝑤 → ∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤))
176		olc 866	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑤 → (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤))
177	176	anim2i 617	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤) → (𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
178	177	eximi 1837	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤) → ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
179	175, 178	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ 𝑤 → ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
180	169, 179	jaoi 855	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ∨ 𝑣 ∈ 𝑤) → ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
181		eluni 4868	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ ∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})))
182		elun 4108	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ (𝑦 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∨ 𝑦 ∈ {𝑤}))
183		eliun 4958	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ↔ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠))
184		velsn 4602	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ {𝑤} ↔ 𝑦 = 𝑤)
185	183, 184	orbi12i 913	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∨ 𝑦 ∈ {𝑤}) ↔ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤))
186	182, 185	bitri 274	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤))
187	186	anbi2i 623	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑣 ∈ 𝑦 ∧ 𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})) ↔ (𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
188	187	exbii 1850	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})) ↔ ∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)))
189	181, 188	bitr2i 275	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ (∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠) ∨ 𝑦 = 𝑤)) ↔ 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
190	180, 189	sylib 217	. . . . . . . . . . . . . . . . . 18 ⊢ ((∃𝑦(𝑣 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝑡 𝑦 ∈ (𝑓‘𝑠)) ∨ 𝑣 ∈ 𝑤) → 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
191	166, 190	syl6 35	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 = ∩ 𝑡 ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → (𝑣 ∈ 𝑋 → 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})))
192	191	ad5ant25 760	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → (𝑣 ∈ 𝑋 → 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})))
193	192	ad2ant2l 744	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (𝑣 ∈ 𝑋 → 𝑣 ∈ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})))
194	193	ssrdv 3950	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑋 ⊆ ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
195		elun 4108	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ (𝑣 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∨ 𝑣 ∈ {𝑤}))
196		eliun 4958	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ↔ ∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠))
197		velsn 4602	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ∈ {𝑤} ↔ 𝑣 = 𝑤)
198	196, 197	orbi12i 913	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 ∈ ∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∨ 𝑣 ∈ {𝑤}) ↔ (∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) ∨ 𝑣 = 𝑤))
199	195, 198	bitri 274	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ↔ (∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) ∨ 𝑣 = 𝑤))
200		nfra1 3267	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑠∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)
201		nfv 1917	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑠 𝑣 ⊆ 𝑋
202		rsp 3230	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (𝑠 ∈ 𝑡 → 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)))
203		eqimss2 4001	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (∪ (𝑓‘𝑠) ∪ 𝑠) ⊆ 𝑋)
204		elssuni 4898	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ ∪ (𝑓‘𝑠))
205		ssun3 4134	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ⊆ ∪ (𝑓‘𝑠) → 𝑣 ⊆ (∪ (𝑓‘𝑠) ∪ 𝑠))
206	204, 205	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ (∪ (𝑓‘𝑠) ∪ 𝑠))
207		sstr 3952	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 ⊆ (∪ (𝑓‘𝑠) ∪ 𝑠) ∧ (∪ (𝑓‘𝑠) ∪ 𝑠) ⊆ 𝑋) → 𝑣 ⊆ 𝑋)
208	207	expcom 414	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((∪ (𝑓‘𝑠) ∪ 𝑠) ⊆ 𝑋 → (𝑣 ⊆ (∪ (𝑓‘𝑠) ∪ 𝑠) → 𝑣 ⊆ 𝑋))
209	203, 206, 208	syl2im 40	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ 𝑋))
210	202, 209	syl6 35	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (𝑠 ∈ 𝑡 → (𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ 𝑋)))
211	200, 201, 210	rexlimd 3249	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠) → (∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ 𝑋))
212	211	ad2antll 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) → 𝑣 ⊆ 𝑋))
213		elpwi 4567	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑢 ∈ 𝒫 (fi‘𝑥) → 𝑢 ⊆ (fi‘𝑥))
214	213	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) → 𝑢 ⊆ (fi‘𝑥))
215	214	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑢 ⊆ (fi‘𝑥))
216	215, 99	sseldd 3945	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑤 ∈ (fi‘𝑥))
217		elssuni 4898	. . . . . . . . . . . . . . . . . . . . 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 2793	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → ∪ (fi‘𝑥) = ∪ 𝐽)
221	220, 66	eqtr4di 2794	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → ∪ (fi‘𝑥) = 𝑋)
222	221	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → ∪ (fi‘𝑥) = 𝑋)
223	222	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∪ (fi‘𝑥) = 𝑋)
224	218, 223	sseqtrd 3984	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑤 ⊆ 𝑋)
225		sseq1 3969	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = 𝑤 → (𝑣 ⊆ 𝑋 ↔ 𝑤 ⊆ 𝑋))
226	224, 225	syl5ibrcom 246	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (𝑣 = 𝑤 → 𝑣 ⊆ 𝑋))
227	212, 226	jaod 857	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ((∃𝑠 ∈ 𝑡 𝑣 ∈ (𝑓‘𝑠) ∨ 𝑣 = 𝑤) → 𝑣 ⊆ 𝑋))
228	199, 227	biimtrid 241	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → (𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) → 𝑣 ⊆ 𝑋))
229	228	ralrimiv 3142	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∀𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})𝑣 ⊆ 𝑋)
230		unissb 4900	. . . . . . . . . . . . . . 15 ⊢ (∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑋 ↔ ∀𝑣 ∈ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})𝑣 ⊆ 𝑋)
231	229, 230	sylibr 233	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ⊆ 𝑋)
232	194, 231	eqssd 3961	. . . . . . . . . . . . 13 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → 𝑋 = ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
233		unieq 4876	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) → ∪ 𝑏 = ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}))
234	233	rspceeqv 3595	. . . . . . . . . . . . 13 ⊢ (((∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = ∪ (∪ 𝑠 ∈ 𝑡 (𝑓‘𝑠) ∪ {𝑤})) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏)
235	116, 232, 234	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) ∧ (𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠))) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏)
236	235	ex 413	. . . . . . . . . . 11 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → ((𝑓:𝑡⟶(𝒫 𝑢 ∩ Fin) ∧ ∀𝑠 ∈ 𝑡 𝑋 = (∪ (𝑓‘𝑠) ∪ 𝑠)) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏))
237	236	exlimdv 1936	. . . . . . . . . 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 241	. . . . . . . 8 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ 𝑎 ⊆ 𝑢)) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) ∧ 𝑤 ∈ 𝑢)) → (¬ ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛 → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏))
240		dfrex2 3076	. . . . . . . 8 ⊢ (∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏 ↔ ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)
241	239, 240	syl6ib 250	. . . . . . 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 421	. . . . 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 421	. . 3 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (𝑢 ∈ 𝒫 (fi‘𝑥) → (𝑎 ⊆ 𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → (𝑤 ∈ 𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))))))
246	245	imp45 430	. 2 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑤 ∈ 𝑢 → (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)))
247	246	imp31 418	1 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∧ w3a 1087  ∀wal 1539   = wceq 1541  ∃wex 1781   ∈ wcel 2106  ∀wral 3064  ∃wrex 3073  Vcvv 3445   ∖ cdif 3907   ∪ cun 3908   ∩ cin 3909   ⊆ wss 3910  𝒫 cpw 4560  {csn 4586  ∪ cuni 4865  ∩ cint 4907  ∪ ciun 4954  ⟶wf 6492  ‘cfv 6496  Fincfn 8883  ficfi 9346  topGenctg 17319  TopBasesctb 22295

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-om 7803  df-1o 8412  df-er 8648  df-en 8884  df-fin 8887  df-fi 9347  df-topgen 17325  df-bases 22296

This theorem is referenced by:  alexsubALTlem4  23401