Theorem alexsubALTlem4 23401

Description: Lemma for alexsubALT 23402. If any cover taken from a subbase has a finite subcover, any cover taken from the corresponding base has a finite subcover. (Contributed by Jeff Hankins, 28-Jan-2010.) (Revised by Mario Carneiro, 14-Dec-2013.)

Hypothesis

Ref	Expression
alexsubALT.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
alexsubALTlem4	⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → ∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))

Distinct variable groups:   𝑎,𝑏,𝑐,𝑑,𝑥,𝐽   𝑋,𝑎,𝑏,𝑐,𝑑,𝑥

Proof of Theorem alexsubALTlem4

Dummy variables 𝑛 𝑠 𝑡 𝑢 𝑣 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ralnex 3075	. . . . 5 ⊢ (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 ↔ ¬ ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)
2		alexsubALT.1	. . . . . . . 8 ⊢ 𝑋 = ∪ 𝐽
3	2	alexsubALTlem2 23399	. . . . . . 7 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → ∃𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣)
4		elun 4108	. . . . . . . . . 10 ⊢ (𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ↔ (𝑢 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∨ 𝑢 ∈ {∅}))
5		sseq2 3970	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑢 → (𝑎 ⊆ 𝑧 ↔ 𝑎 ⊆ 𝑢))
6		pweq 4574	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑢 → 𝒫 𝑧 = 𝒫 𝑢)
7	6	ineq1d 4171	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑢 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑢 ∩ Fin))
8	7	raleqdv 3313	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑢 → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 ↔ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))
9	5, 8	anbi12d 631	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑢 → ((𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ↔ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
10	9	elrab 3645	. . . . . . . . . . 11 ⊢ (𝑢 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ↔ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
11		velsn 4602	. . . . . . . . . . 11 ⊢ (𝑢 ∈ {∅} ↔ 𝑢 = ∅)
12	10, 11	orbi12i 913	. . . . . . . . . 10 ⊢ ((𝑢 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∨ 𝑢 ∈ {∅}) ↔ ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) ∨ 𝑢 = ∅))
13	4, 12	bitri 274	. . . . . . . . 9 ⊢ (𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ↔ ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) ∨ 𝑢 = ∅))
14		ralnex 3075	. . . . . . . . . . . . 13 ⊢ (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 ↔ ¬ ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣)
15		simprrl 779	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → 𝑎 ⊆ 𝑢)
16	15	unissd 4875	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → ∪ 𝑎 ⊆ ∪ 𝑢)
17		sseq1 3969	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 = ∪ 𝑎 → (𝑋 ⊆ ∪ 𝑢 ↔ ∪ 𝑎 ⊆ ∪ 𝑢))
18	16, 17	syl5ibrcom 246	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑋 = ∪ 𝑎 → 𝑋 ⊆ ∪ 𝑢))
19		vex 3449	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑥 ∈ V
20		inss1 4188	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∩ 𝑢) ⊆ 𝑥
21	19, 20	elpwi2 5303	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∩ 𝑢) ∈ 𝒫 𝑥
22		unieq 4876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 = (𝑥 ∩ 𝑢) → ∪ 𝑐 = ∪ (𝑥 ∩ 𝑢))
23	22	eqeq2d 2747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 = (𝑥 ∩ 𝑢) → (𝑋 = ∪ 𝑐 ↔ 𝑋 = ∪ (𝑥 ∩ 𝑢)))
24		pweq 4574	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑐 = (𝑥 ∩ 𝑢) → 𝒫 𝑐 = 𝒫 (𝑥 ∩ 𝑢))
25	24	ineq1d 4171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 = (𝑥 ∩ 𝑢) → (𝒫 𝑐 ∩ Fin) = (𝒫 (𝑥 ∩ 𝑢) ∩ Fin))
26	25	rexeqdv 3314	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 = (𝑥 ∩ 𝑢) → (∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑 ↔ ∃𝑑 ∈ (𝒫 (𝑥 ∩ 𝑢) ∩ Fin)𝑋 = ∪ 𝑑))
27	23, 26	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 = (𝑥 ∩ 𝑢) → ((𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ↔ (𝑋 = ∪ (𝑥 ∩ 𝑢) → ∃𝑑 ∈ (𝒫 (𝑥 ∩ 𝑢) ∩ Fin)𝑋 = ∪ 𝑑)))
28	27	rspccv 3578	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → ((𝑥 ∩ 𝑢) ∈ 𝒫 𝑥 → (𝑋 = ∪ (𝑥 ∩ 𝑢) → ∃𝑑 ∈ (𝒫 (𝑥 ∩ 𝑢) ∩ Fin)𝑋 = ∪ 𝑑)))
29	21, 28	mpi 20	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → (𝑋 = ∪ (𝑥 ∩ 𝑢) → ∃𝑑 ∈ (𝒫 (𝑥 ∩ 𝑢) ∩ Fin)𝑋 = ∪ 𝑑))
30		inss2 4189	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∩ 𝑢) ⊆ 𝑢
31		sstr 3952	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑑 ⊆ (𝑥 ∩ 𝑢) ∧ (𝑥 ∩ 𝑢) ⊆ 𝑢) → 𝑑 ⊆ 𝑢)
32	30, 31	mpan2 689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑑 ⊆ (𝑥 ∩ 𝑢) → 𝑑 ⊆ 𝑢)
33	32	anim1i 615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑑 ⊆ (𝑥 ∩ 𝑢) ∧ 𝑑 ∈ Fin) → (𝑑 ⊆ 𝑢 ∧ 𝑑 ∈ Fin))
34		elfpw 9298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑑 ∈ (𝒫 (𝑥 ∩ 𝑢) ∩ Fin) ↔ (𝑑 ⊆ (𝑥 ∩ 𝑢) ∧ 𝑑 ∈ Fin))
35		elfpw 9298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑑 ∈ (𝒫 𝑢 ∩ Fin) ↔ (𝑑 ⊆ 𝑢 ∧ 𝑑 ∈ Fin))
36	33, 34, 35	3imtr4i 291	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑑 ∈ (𝒫 (𝑥 ∩ 𝑢) ∩ Fin) → 𝑑 ∈ (𝒫 𝑢 ∩ Fin))
37	36	anim1i 615	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑑 ∈ (𝒫 (𝑥 ∩ 𝑢) ∩ Fin) ∧ 𝑋 = ∪ 𝑑) → (𝑑 ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = ∪ 𝑑))
38	37	reximi2 3082	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑑 ∈ (𝒫 (𝑥 ∩ 𝑢) ∩ Fin)𝑋 = ∪ 𝑑 → ∃𝑑 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑑)
39	29, 38	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → (𝑋 = ∪ (𝑥 ∩ 𝑢) → ∃𝑑 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑑))
40		unieq 4876	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑑 = 𝑏 → ∪ 𝑑 = ∪ 𝑏)
41	40	eqeq2d 2747	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = 𝑏 → (𝑋 = ∪ 𝑑 ↔ 𝑋 = ∪ 𝑏))
42	41	cbvrexvw 3226	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∃𝑑 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑑 ↔ ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏)
43	39, 42	syl6ib 250	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → (𝑋 = ∪ (𝑥 ∩ 𝑢) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏))
44		dfrex2 3076	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏 ↔ ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)
45	43, 44	syl6ib 250	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → (𝑋 = ∪ (𝑥 ∩ 𝑢) → ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))
46	45	con2d 134	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ (𝑥 ∩ 𝑢)))
47	46	a1d 25	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → (𝑎 ⊆ 𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ (𝑥 ∩ 𝑢))))
48	47	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (𝑎 ⊆ 𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ (𝑥 ∩ 𝑢))))
49	48	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ 𝑢 ∈ 𝒫 (fi‘𝑥)) → (𝑎 ⊆ 𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ (𝑥 ∩ 𝑢))))
50	49	impd 411	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ 𝑢 ∈ 𝒫 (fi‘𝑥)) → ((𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → ¬ 𝑋 = ∪ (𝑥 ∩ 𝑢)))
51	50	impr 455	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → ¬ 𝑋 = ∪ (𝑥 ∩ 𝑢))
52	20	unissi 4874	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ (𝑥 ∩ 𝑢) ⊆ ∪ 𝑥
53		fiuni 9364	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ V → ∪ 𝑥 = ∪ (fi‘𝑥))
54	53	elv 3451	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ 𝑥 = ∪ (fi‘𝑥)
55		fibas 22327	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (fi‘𝑥) ∈ TopBases
56		unitg 22317	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((fi‘𝑥) ∈ TopBases → ∪ (topGen‘(fi‘𝑥)) = ∪ (fi‘𝑥))
57	55, 56	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ (topGen‘(fi‘𝑥)) = ∪ (fi‘𝑥)
58	54, 57	eqtr4i 2767	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∪ 𝑥 = ∪ (topGen‘(fi‘𝑥))
59		unieq 4876	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → ∪ 𝐽 = ∪ (topGen‘(fi‘𝑥)))
60	58, 59	eqtr4id 2795	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → ∪ 𝑥 = ∪ 𝐽)
61	60, 2	eqtr4di 2794	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → ∪ 𝑥 = 𝑋)
62	61	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → ∪ 𝑥 = 𝑋)
63	62	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → ∪ 𝑥 = 𝑋)
64	52, 63	sseqtrid 3996	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → ∪ (𝑥 ∩ 𝑢) ⊆ 𝑋)
65		eqcom 2743	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋 = ∪ (𝑥 ∩ 𝑢) ↔ ∪ (𝑥 ∩ 𝑢) = 𝑋)
66		eqss 3959	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∪ (𝑥 ∩ 𝑢) = 𝑋 ↔ (∪ (𝑥 ∩ 𝑢) ⊆ 𝑋 ∧ 𝑋 ⊆ ∪ (𝑥 ∩ 𝑢)))
67	66	baib 536	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ (𝑥 ∩ 𝑢) ⊆ 𝑋 → (∪ (𝑥 ∩ 𝑢) = 𝑋 ↔ 𝑋 ⊆ ∪ (𝑥 ∩ 𝑢)))
68	65, 67	bitrid 282	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ (𝑥 ∩ 𝑢) ⊆ 𝑋 → (𝑋 = ∪ (𝑥 ∩ 𝑢) ↔ 𝑋 ⊆ ∪ (𝑥 ∩ 𝑢)))
69	64, 68	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑋 = ∪ (𝑥 ∩ 𝑢) ↔ 𝑋 ⊆ ∪ (𝑥 ∩ 𝑢)))
70	51, 69	mtbid 323	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → ¬ 𝑋 ⊆ ∪ (𝑥 ∩ 𝑢))
71		sstr2 3951	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ⊆ ∪ 𝑢 → (∪ 𝑢 ⊆ ∪ (𝑥 ∩ 𝑢) → 𝑋 ⊆ ∪ (𝑥 ∩ 𝑢)))
72	71	con3rr3 155	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑋 ⊆ ∪ (𝑥 ∩ 𝑢) → (𝑋 ⊆ ∪ 𝑢 → ¬ ∪ 𝑢 ⊆ ∪ (𝑥 ∩ 𝑢)))
73	70, 72	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑋 ⊆ ∪ 𝑢 → ¬ ∪ 𝑢 ⊆ ∪ (𝑥 ∩ 𝑢)))
74		nss 4006	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ∪ 𝑢 ⊆ ∪ (𝑥 ∩ 𝑢) ↔ ∃𝑦(𝑦 ∈ ∪ 𝑢 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))
75		df-rex 3074	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑦 ∈ ∪ 𝑢 ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) ↔ ∃𝑦(𝑦 ∈ ∪ 𝑢 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))
76	74, 75	bitr4i 277	. . . . . . . . . . . . . . . 16 ⊢ (¬ ∪ 𝑢 ⊆ ∪ (𝑥 ∩ 𝑢) ↔ ∃𝑦 ∈ ∪ 𝑢 ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))
77		eluni2 4869	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ∪ 𝑢 ↔ ∃𝑤 ∈ 𝑢 𝑦 ∈ 𝑤)
78		elpwi 4567	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ 𝒫 (fi‘𝑥) → 𝑢 ⊆ (fi‘𝑥))
79	78	sseld 3943	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ 𝒫 (fi‘𝑥) → (𝑤 ∈ 𝑢 → 𝑤 ∈ (fi‘𝑥)))
80	79	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑤 ∈ 𝑢 → 𝑤 ∈ (fi‘𝑥)))
81		elfi 9349	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑤 ∈ V ∧ 𝑥 ∈ V) → (𝑤 ∈ (fi‘𝑥) ↔ ∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = ∩ 𝑡))
82	81	el2v 3453	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ (fi‘𝑥) ↔ ∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = ∩ 𝑡)
83	80, 82	syl6ib 250	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑤 ∈ 𝑢 → ∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = ∩ 𝑡))
84	2	alexsubALTlem3 23400	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)
85	78	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) → 𝑢 ⊆ (fi‘𝑥))
86	85	ad4antlr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑢 ⊆ (fi‘𝑥))
87		ssfii 9355	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥 ∈ V → 𝑥 ⊆ (fi‘𝑥))
88	87	elv 3451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑥 ⊆ (fi‘𝑥)
89		elinel1 4155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ 𝒫 𝑥)
90	89	elpwid 4569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ⊆ 𝑥)
91	90	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) → 𝑡 ⊆ 𝑥)
92	91	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑡 ⊆ 𝑥)
93		simprl 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑠 ∈ 𝑡)
94	92, 93	sseldd 3945	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑠 ∈ 𝑥)
95	88, 94	sselid 3942	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑠 ∈ (fi‘𝑥))
96	95	snssd 4769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → {𝑠} ⊆ (fi‘𝑥))
97	86, 96	unssd 4146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → (𝑢 ∪ {𝑠}) ⊆ (fi‘𝑥))
98		fvex 6855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (fi‘𝑥) ∈ V
99	98	elpw2 5302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑢 ∪ {𝑠}) ∈ 𝒫 (fi‘𝑥) ↔ (𝑢 ∪ {𝑠}) ⊆ (fi‘𝑥))
100	97, 99	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → (𝑢 ∪ {𝑠}) ∈ 𝒫 (fi‘𝑥))
101		simprl 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) → 𝑎 ⊆ 𝑢)
102	101	ad4antlr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑎 ⊆ 𝑢)
103		ssun1 4132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 𝑢 ⊆ (𝑢 ∪ {𝑠})
104	102, 103	sstrdi 3956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑎 ⊆ (𝑢 ∪ {𝑠}))
105		unieq 4876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑛 = 𝑏 → ∪ 𝑛 = ∪ 𝑏)
106	105	eqeq2d 2747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑛 = 𝑏 → (𝑋 = ∪ 𝑛 ↔ 𝑋 = ∪ 𝑏))
107	106	notbid 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 = 𝑏 → (¬ 𝑋 = ∪ 𝑛 ↔ ¬ 𝑋 = ∪ 𝑏))
108	107	cbvralvw 3225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛 ↔ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑏)
109	108	biimpi 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛 → ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑏)
110	109	ad2antll 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑏)
111	100, 104, 110	jca32 516	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → ((𝑢 ∪ {𝑠}) ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ (𝑢 ∪ {𝑠}) ∧ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
112		sseq2 3970	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = (𝑢 ∪ {𝑠}) → (𝑎 ⊆ 𝑧 ↔ 𝑎 ⊆ (𝑢 ∪ {𝑠})))
113		pweq 4574	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 = (𝑢 ∪ {𝑠}) → 𝒫 𝑧 = 𝒫 (𝑢 ∪ {𝑠}))
114	113	ineq1d 4171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 = (𝑢 ∪ {𝑠}) → (𝒫 𝑧 ∩ Fin) = (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin))
115	114	raleqdv 3313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = (𝑢 ∪ {𝑠}) → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 ↔ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑏))
116	112, 115	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = (𝑢 ∪ {𝑠}) → ((𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ↔ (𝑎 ⊆ (𝑢 ∪ {𝑠}) ∧ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
117	116	elrab 3645	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑢 ∪ {𝑠}) ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ↔ ((𝑢 ∪ {𝑠}) ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ (𝑢 ∪ {𝑠}) ∧ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
118	111, 117	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → (𝑢 ∪ {𝑠}) ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)})
119		elun1 4136	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑢 ∪ {𝑠}) ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} → (𝑢 ∪ {𝑠}) ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}))
120	118, 119	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → (𝑢 ∪ {𝑠}) ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}))
121		vsnid 4623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑠 ∈ {𝑠}
122		elun2 4137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑠 ∈ {𝑠} → 𝑠 ∈ (𝑢 ∪ {𝑠}))
123	121, 122	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝑠 ∈ (𝑢 ∪ {𝑠})
124		intss1 4924	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑠 ∈ 𝑡 → ∩ 𝑡 ⊆ 𝑠)
125		sseq1 3969	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑤 = ∩ 𝑡 → (𝑤 ⊆ 𝑠 ↔ ∩ 𝑡 ⊆ 𝑠))
126	124, 125	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑠 ∈ 𝑡 → (𝑤 = ∩ 𝑡 → 𝑤 ⊆ 𝑠))
127	126	impcom 408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑤 = ∩ 𝑡 ∧ 𝑠 ∈ 𝑡) → 𝑤 ⊆ 𝑠)
128	127	ad4ant24 752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ 𝑠 ∈ 𝑡) → 𝑤 ⊆ 𝑠)
129	128	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑤 ∈ 𝑢 ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ 𝑠 ∈ 𝑡)) → 𝑤 ⊆ 𝑠)
130	129	adantrrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑤 ∈ 𝑢 ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → 𝑤 ⊆ 𝑠)
131	130	adantll 712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → 𝑤 ⊆ 𝑠)
132		simprlr 778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → 𝑦 ∈ 𝑤)
133	131, 132	sseldd 3945	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → 𝑦 ∈ 𝑠)
134	90	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) → 𝑡 ⊆ 𝑥)
135	134	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → 𝑡 ⊆ 𝑥)
136		simprrl 779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → 𝑠 ∈ 𝑡)
137	135, 136	sseldd 3945	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → 𝑠 ∈ 𝑥)
138		elin 3926	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑠 ∈ (𝑥 ∩ 𝑢) ↔ (𝑠 ∈ 𝑥 ∧ 𝑠 ∈ 𝑢))
139		elunii 4870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑦 ∈ 𝑠 ∧ 𝑠 ∈ (𝑥 ∩ 𝑢)) → 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))
140	139	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑦 ∈ 𝑠 → (𝑠 ∈ (𝑥 ∩ 𝑢) → 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))
141	138, 140	biimtrrid 242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑦 ∈ 𝑠 → ((𝑠 ∈ 𝑥 ∧ 𝑠 ∈ 𝑢) → 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))
142	141	expd 416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 ∈ 𝑠 → (𝑠 ∈ 𝑥 → (𝑠 ∈ 𝑢 → 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))))
143	133, 137, 142	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → (𝑠 ∈ 𝑢 → 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))
144	143	con3d 152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ¬ 𝑠 ∈ 𝑢))
145	144	expr 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤)) → ((𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛) → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ¬ 𝑠 ∈ 𝑢)))
146	145	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤)) → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ((𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛) → ¬ 𝑠 ∈ 𝑢)))
147	146	exp32 421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) → ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) → (𝑦 ∈ 𝑤 → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ((𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛) → ¬ 𝑠 ∈ 𝑢)))))
148	147	imp55 443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → ¬ 𝑠 ∈ 𝑢)
149		vex 3449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑠 ∈ V
150		eleq1w 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑣 = 𝑠 → (𝑣 ∈ (𝑢 ∪ {𝑠}) ↔ 𝑠 ∈ (𝑢 ∪ {𝑠})))
151		elequ1 2113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑣 = 𝑠 → (𝑣 ∈ 𝑢 ↔ 𝑠 ∈ 𝑢))
152	151	notbid 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑣 = 𝑠 → (¬ 𝑣 ∈ 𝑢 ↔ ¬ 𝑠 ∈ 𝑢))
153	150, 152	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑣 = 𝑠 → ((𝑣 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑣 ∈ 𝑢) ↔ (𝑠 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑠 ∈ 𝑢)))
154	149, 153	spcev 3565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑠 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑠 ∈ 𝑢) → ∃𝑣(𝑣 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑣 ∈ 𝑢))
155	123, 148, 154	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → ∃𝑣(𝑣 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑣 ∈ 𝑢))
156		nss 4006	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (¬ (𝑢 ∪ {𝑠}) ⊆ 𝑢 ↔ ∃𝑣(𝑣 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑣 ∈ 𝑢))
157	155, 156	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → ¬ (𝑢 ∪ {𝑠}) ⊆ 𝑢)
158		eqimss2 4001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑢 = (𝑢 ∪ {𝑠}) → (𝑢 ∪ {𝑠}) ⊆ 𝑢)
159	158	necon3bi 2970	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (¬ (𝑢 ∪ {𝑠}) ⊆ 𝑢 → 𝑢 ≠ (𝑢 ∪ {𝑠}))
160	157, 159	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑢 ≠ (𝑢 ∪ {𝑠}))
161	160, 103	jctil 520	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → (𝑢 ⊆ (𝑢 ∪ {𝑠}) ∧ 𝑢 ≠ (𝑢 ∪ {𝑠})))
162		df-pss 3929	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 ⊊ (𝑢 ∪ {𝑠}) ↔ (𝑢 ⊆ (𝑢 ∪ {𝑠}) ∧ 𝑢 ≠ (𝑢 ∪ {𝑠})))
163	161, 162	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑢 ⊊ (𝑢 ∪ {𝑠}))
164		psseq2 4048	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑣 = (𝑢 ∪ {𝑠}) → (𝑢 ⊊ 𝑣 ↔ 𝑢 ⊊ (𝑢 ∪ {𝑠})))
165	164	rspcev 3581	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑢 ∪ {𝑠}) ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧ 𝑢 ⊊ (𝑢 ∪ {𝑠})) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣)
166	120, 163, 165	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣)
167	84, 166	rexlimddv 3158	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣)
168	167	exp45 439	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) → ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) → (𝑦 ∈ 𝑤 → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣))))
169	168	expd 416	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) → (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → (𝑤 = ∩ 𝑡 → (𝑦 ∈ 𝑤 → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣)))))
170	169	rexlimdv 3150	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) → (∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = ∩ 𝑡 → (𝑦 ∈ 𝑤 → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣))))
171	170	ex 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑤 ∈ 𝑢 → (∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = ∩ 𝑡 → (𝑦 ∈ 𝑤 → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣)))))
172	83, 171	mpdd 43	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑤 ∈ 𝑢 → (𝑦 ∈ 𝑤 → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣))))
173	172	rexlimdv 3150	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (∃𝑤 ∈ 𝑢 𝑦 ∈ 𝑤 → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣)))
174	77, 173	biimtrid 241	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑦 ∈ ∪ 𝑢 → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣)))
175	174	rexlimdv 3150	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (∃𝑦 ∈ ∪ 𝑢 ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣))
176	76, 175	biimtrid 241	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (¬ ∪ 𝑢 ⊆ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣))
177	18, 73, 176	3syld 60	. . . . . . . . . . . . . 14 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑋 = ∪ 𝑎 → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣))
178	177	con3d 152	. . . . . . . . . . . . 13 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (¬ ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎))
179	14, 178	biimtrid 241	. . . . . . . . . . . 12 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎))
180	179	ex 413	. . . . . . . . . . 11 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎)))
181	180	adantr 481	. . . . . . . . . 10 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎)))
182		ssun1 4132	. . . . . . . . . . . . . 14 ⊢ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})
183		eqimss2 4001	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑎 → 𝑎 ⊆ 𝑧)
184	183	biantrurd 533	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑎 → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 ↔ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
185		pweq 4574	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑎 → 𝒫 𝑧 = 𝒫 𝑎)
186	185	ineq1d 4171	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑎 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑎 ∩ Fin))
187	186	raleqdv 3313	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑎 → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 ↔ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))
188	184, 187	bitr3d 280	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑎 → ((𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ↔ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))
189		simpll3 1214	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → 𝑎 ∈ 𝒫 (fi‘𝑥))
190		simplr 767	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)
191	188, 189, 190	elrabd 3647	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → 𝑎 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)})
192	182, 191	sselid 3942	. . . . . . . . . . . . 13 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → 𝑎 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}))
193		psseq2 4048	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑎 → (𝑢 ⊊ 𝑣 ↔ 𝑢 ⊊ 𝑎))
194	193	notbid 317	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑎 → (¬ 𝑢 ⊊ 𝑣 ↔ ¬ 𝑢 ⊊ 𝑎))
195	194	rspcv 3577	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑢 ⊊ 𝑎))
196	192, 195	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑢 ⊊ 𝑎))
197		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ∅ → 𝑎 = ∅)
198		0elpw 5311	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ 𝒫 𝑎
199		0fin 9115	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ Fin
200	198, 199	elini 4153	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ (𝒫 𝑎 ∩ Fin)
201	197, 200	eqeltrdi 2846	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ∅ → 𝑎 ∈ (𝒫 𝑎 ∩ Fin))
202		unieq 4876	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 𝑎 → ∪ 𝑏 = ∪ 𝑎)
203	202	eqeq2d 2747	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑎 → (𝑋 = ∪ 𝑏 ↔ 𝑋 = ∪ 𝑎))
204	203	notbid 317	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑎 → (¬ 𝑋 = ∪ 𝑏 ↔ ¬ 𝑋 = ∪ 𝑎))
205	204	rspccv 3578	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → (𝑎 ∈ (𝒫 𝑎 ∩ Fin) → ¬ 𝑋 = ∪ 𝑎))
206	201, 205	syl5 34	. . . . . . . . . . . . . . 15 ⊢ (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → (𝑎 = ∅ → ¬ 𝑋 = ∪ 𝑎))
207	206	necon2ad 2958	. . . . . . . . . . . . . 14 ⊢ (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → (𝑋 = ∪ 𝑎 → 𝑎 ≠ ∅))
208	207	ad2antlr 725	. . . . . . . . . . . . 13 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → (𝑋 = ∪ 𝑎 → 𝑎 ≠ ∅))
209		psseq1 4047	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = ∅ → (𝑢 ⊊ 𝑎 ↔ ∅ ⊊ 𝑎))
210	209	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → (𝑢 ⊊ 𝑎 ↔ ∅ ⊊ 𝑎))
211		0pss 4404	. . . . . . . . . . . . . 14 ⊢ (∅ ⊊ 𝑎 ↔ 𝑎 ≠ ∅)
212	210, 211	bitrdi 286	. . . . . . . . . . . . 13 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → (𝑢 ⊊ 𝑎 ↔ 𝑎 ≠ ∅))
213	208, 212	sylibrd 258	. . . . . . . . . . . 12 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → (𝑋 = ∪ 𝑎 → 𝑢 ⊊ 𝑎))
214	196, 213	nsyld 156	. . . . . . . . . . 11 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎))
215	214	ex 413	. . . . . . . . . 10 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → (𝑢 = ∅ → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎)))
216	181, 215	jaod 857	. . . . . . . . 9 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → (((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) ∨ 𝑢 = ∅) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎)))
217	13, 216	biimtrid 241	. . . . . . . 8 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → (𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎)))
218	217	rexlimdv 3150	. . . . . . 7 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → (∃𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎))
219	3, 218	mpd 15	. . . . . 6 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → ¬ 𝑋 = ∪ 𝑎)
220	219	ex 413	. . . . 5 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ 𝑎))
221	1, 220	biimtrrid 242	. . . 4 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (¬ ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ 𝑎))
222	221	con4d 115	. . 3 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
223	222	3exp 1119	. 2 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → (𝑎 ∈ 𝒫 (fi‘𝑥) → (𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))))
224	223	ralrimdv 3149	1 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → ∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∧ w3a 1087   = wceq 1541  ∃wex 1781   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3073  {crab 3407  Vcvv 3445   ∪ cun 3908   ∩ cin 3909   ⊆ wss 3910   ⊊ wpss 3911  ∅c0 4282  𝒫 cpw 4560  {csn 4586  ∪ cuni 4865  ∩ cint 4907  ‘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-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-ac2 10399

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-rmo 3353  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-se 5589  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-pred 6253  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-isom 6505  df-riota 7313  df-ov 7360  df-rpss 7660  df-om 7803  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-1o 8412  df-er 8648  df-en 8884  df-fin 8887  df-fi 9347  df-card 9875  df-ac 10052  df-topgen 17325  df-bases 22296

This theorem is referenced by:  alexsubALT  23402