Theorem alexsubALTlem4 24168

Description: Lemma for alexsubALT 24169. 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 3091	. . . . 5 ⊢ (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 ↔ ¬ ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)
2		alexsubALT.1	. . . . . . . 8 ⊢ 𝑋 = ∪ 𝐽
3	2	alexsubALTlem2 24166	. . . . . . 7 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → ∃𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣)
4		elun 4109	. . . . . . . . . 10 ⊢ (𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ↔ (𝑢 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∨ 𝑢 ∈ {∅}))
5		sseq2 3965	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑢 → (𝑎 ⊆ 𝑧 ↔ 𝑎 ⊆ 𝑢))
6		pweq 4572	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑢 → 𝒫 𝑧 = 𝒫 𝑢)
7	6	ineq1d 4174	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑢 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑢 ∩ Fin))
8	7	raleqdv 3323	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑢 → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 ↔ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))
9	5, 8	anbi12d 643	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑢 → ((𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ↔ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
10	9	elrab 3653	. . . . . . . . . . 11 ⊢ (𝑢 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ↔ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
11		velsn 4601	. . . . . . . . . . 11 ⊢ (𝑢 ∈ {∅} ↔ 𝑢 = ∅)
12	10, 11	orbi12i 927	. . . . . . . . . 10 ⊢ ((𝑢 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∨ 𝑢 ∈ {∅}) ↔ ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) ∨ 𝑢 = ∅))
13	4, 12	bitri 278	. . . . . . . . 9 ⊢ (𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ↔ ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) ∨ 𝑢 = ∅))
14		ralnex 3091	. . . . . . . . . . . . 13 ⊢ (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 ↔ ¬ ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣)
15		simprrl 792	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → 𝑎 ⊆ 𝑢)
16	15	unissd 4878	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → ∪ 𝑎 ⊆ ∪ 𝑢)
17		sseq1 3964	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 = ∪ 𝑎 → (𝑋 ⊆ ∪ 𝑢 ↔ ∪ 𝑎 ⊆ ∪ 𝑢))
18	16, 17	syl5ibrcom 250	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑋 = ∪ 𝑎 → 𝑋 ⊆ ∪ 𝑢))
19		vex 3461	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑥 ∈ V
20		inss1 4191	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∩ 𝑢) ⊆ 𝑥
21	19, 20	elpwi2 5296	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∩ 𝑢) ∈ 𝒫 𝑥
22		unieq 4879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 = (𝑥 ∩ 𝑢) → ∪ 𝑐 = ∪ (𝑥 ∩ 𝑢))
23	22	eqeq2d 2776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 = (𝑥 ∩ 𝑢) → (𝑋 = ∪ 𝑐 ↔ 𝑋 = ∪ (𝑥 ∩ 𝑢)))
24		pweq 4572	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑐 = (𝑥 ∩ 𝑢) → 𝒫 𝑐 = 𝒫 (𝑥 ∩ 𝑢))
25	24	ineq1d 4174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 = (𝑥 ∩ 𝑢) → (𝒫 𝑐 ∩ Fin) = (𝒫 (𝑥 ∩ 𝑢) ∩ Fin))
26	25	rexeqdv 3324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 = (𝑥 ∩ 𝑢) → (∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑 ↔ ∃𝑑 ∈ (𝒫 (𝑥 ∩ 𝑢) ∩ Fin)𝑋 = ∪ 𝑑))
27	23, 26	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 = (𝑥 ∩ 𝑢) → ((𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ↔ (𝑋 = ∪ (𝑥 ∩ 𝑢) → ∃𝑑 ∈ (𝒫 (𝑥 ∩ 𝑢) ∩ Fin)𝑋 = ∪ 𝑑)))
28	27	rspccv 3581	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → ((𝑥 ∩ 𝑢) ∈ 𝒫 𝑥 → (𝑋 = ∪ (𝑥 ∩ 𝑢) → ∃𝑑 ∈ (𝒫 (𝑥 ∩ 𝑢) ∩ Fin)𝑋 = ∪ 𝑑)))
29	21, 28	mpi 21	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → (𝑋 = ∪ (𝑥 ∩ 𝑢) → ∃𝑑 ∈ (𝒫 (𝑥 ∩ 𝑢) ∩ Fin)𝑋 = ∪ 𝑑))
30		inss2 4192	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∩ 𝑢) ⊆ 𝑢
31		sstr 3947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑑 ⊆ (𝑥 ∩ 𝑢) ∧ (𝑥 ∩ 𝑢) ⊆ 𝑢) → 𝑑 ⊆ 𝑢)
32	30, 31	mpan2 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑑 ⊆ (𝑥 ∩ 𝑢) → 𝑑 ⊆ 𝑢)
33	32	anim1i 626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑑 ⊆ (𝑥 ∩ 𝑢) ∧ 𝑑 ∈ Fin) → (𝑑 ⊆ 𝑢 ∧ 𝑑 ∈ Fin))
34		elfpw 9299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑑 ∈ (𝒫 (𝑥 ∩ 𝑢) ∩ Fin) ↔ (𝑑 ⊆ (𝑥 ∩ 𝑢) ∧ 𝑑 ∈ Fin))
35		elfpw 9299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑑 ∈ (𝒫 𝑢 ∩ Fin) ↔ (𝑑 ⊆ 𝑢 ∧ 𝑑 ∈ Fin))
36	33, 34, 35	3imtr4i 295	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑑 ∈ (𝒫 (𝑥 ∩ 𝑢) ∩ Fin) → 𝑑 ∈ (𝒫 𝑢 ∩ Fin))
37	36	anim1i 626	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑑 ∈ (𝒫 (𝑥 ∩ 𝑢) ∩ Fin) ∧ 𝑋 = ∪ 𝑑) → (𝑑 ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = ∪ 𝑑))
38	37	reximi2 3098	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑑 ∈ (𝒫 (𝑥 ∩ 𝑢) ∩ Fin)𝑋 = ∪ 𝑑 → ∃𝑑 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑑)
39	29, 38	syl6 36	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → (𝑋 = ∪ (𝑥 ∩ 𝑢) → ∃𝑑 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑑))
40		unieq 4879	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑑 = 𝑏 → ∪ 𝑑 = ∪ 𝑏)
41	40	eqeq2d 2776	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = 𝑏 → (𝑋 = ∪ 𝑑 ↔ 𝑋 = ∪ 𝑏))
42	41	cbvrexvw 3244	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∃𝑑 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑑 ↔ ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏)
43	39, 42	imbitrdi 254	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → (𝑋 = ∪ (𝑥 ∩ 𝑢) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏))
44		dfrex2 3092	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏 ↔ ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)
45	43, 44	imbitrdi 254	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → (𝑋 = ∪ (𝑥 ∩ 𝑢) → ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))
46	45	con2d 135	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ (𝑥 ∩ 𝑢)))
47	46	a1d 26	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → (𝑎 ⊆ 𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ (𝑥 ∩ 𝑢))))
48	47	3ad2ant2 1150	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (𝑎 ⊆ 𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ (𝑥 ∩ 𝑢))))
49	48	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ 𝑢 ∈ 𝒫 (fi‘𝑥)) → (𝑎 ⊆ 𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ (𝑥 ∩ 𝑢))))
50	49	impd 415	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ 𝑢 ∈ 𝒫 (fi‘𝑥)) → ((𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → ¬ 𝑋 = ∪ (𝑥 ∩ 𝑢)))
51	50	impr 459	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → ¬ 𝑋 = ∪ (𝑥 ∩ 𝑢))
52	20	unissi 4877	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ (𝑥 ∩ 𝑢) ⊆ ∪ 𝑥
53		fiuni 9376	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ V → ∪ 𝑥 = ∪ (fi‘𝑥))
54	53	elv 3462	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ 𝑥 = ∪ (fi‘𝑥)
55		fibas 23095	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (fi‘𝑥) ∈ TopBases
56		unitg 23085	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((fi‘𝑥) ∈ TopBases → ∪ (topGen‘(fi‘𝑥)) = ∪ (fi‘𝑥))
57	55, 56	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ (topGen‘(fi‘𝑥)) = ∪ (fi‘𝑥)
58	54, 57	eqtr4i 2791	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∪ 𝑥 = ∪ (topGen‘(fi‘𝑥))
59		unieq 4879	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → ∪ 𝐽 = ∪ (topGen‘(fi‘𝑥)))
60	58, 59	eqtr4id 2819	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → ∪ 𝑥 = ∪ 𝐽)
61	60, 2	eqtr4di 2818	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → ∪ 𝑥 = 𝑋)
62	61	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → ∪ 𝑥 = 𝑋)
63	62	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → ∪ 𝑥 = 𝑋)
64	52, 63	sseqtrid 3981	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → ∪ (𝑥 ∩ 𝑢) ⊆ 𝑋)
65		eqcom 2772	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋 = ∪ (𝑥 ∩ 𝑢) ↔ ∪ (𝑥 ∩ 𝑢) = 𝑋)
66		eqss 3954	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∪ (𝑥 ∩ 𝑢) = 𝑋 ↔ (∪ (𝑥 ∩ 𝑢) ⊆ 𝑋 ∧ 𝑋 ⊆ ∪ (𝑥 ∩ 𝑢)))
67	66	baib 544	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ (𝑥 ∩ 𝑢) ⊆ 𝑋 → (∪ (𝑥 ∩ 𝑢) = 𝑋 ↔ 𝑋 ⊆ ∪ (𝑥 ∩ 𝑢)))
68	65, 67	bitrid 286	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ (𝑥 ∩ 𝑢) ⊆ 𝑋 → (𝑋 = ∪ (𝑥 ∩ 𝑢) ↔ 𝑋 ⊆ ∪ (𝑥 ∩ 𝑢)))
69	64, 68	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑋 = ∪ (𝑥 ∩ 𝑢) ↔ 𝑋 ⊆ ∪ (𝑥 ∩ 𝑢)))
70	51, 69	mtbid 327	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → ¬ 𝑋 ⊆ ∪ (𝑥 ∩ 𝑢))
71		sstr2 3946	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ⊆ ∪ 𝑢 → (∪ 𝑢 ⊆ ∪ (𝑥 ∩ 𝑢) → 𝑋 ⊆ ∪ (𝑥 ∩ 𝑢)))
72	71	con3rr3 156	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑋 ⊆ ∪ (𝑥 ∩ 𝑢) → (𝑋 ⊆ ∪ 𝑢 → ¬ ∪ 𝑢 ⊆ ∪ (𝑥 ∩ 𝑢)))
73	70, 72	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑋 ⊆ ∪ 𝑢 → ¬ ∪ 𝑢 ⊆ ∪ (𝑥 ∩ 𝑢)))
74		nss 4003	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ∪ 𝑢 ⊆ ∪ (𝑥 ∩ 𝑢) ↔ ∃𝑦(𝑦 ∈ ∪ 𝑢 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))
75		df-rex 3090	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑦 ∈ ∪ 𝑢 ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) ↔ ∃𝑦(𝑦 ∈ ∪ 𝑢 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))
76	74, 75	bitr4i 281	. . . . . . . . . . . . . . . 16 ⊢ (¬ ∪ 𝑢 ⊆ ∪ (𝑥 ∩ 𝑢) ↔ ∃𝑦 ∈ ∪ 𝑢 ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))
77		eluni2 4872	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ∪ 𝑢 ↔ ∃𝑤 ∈ 𝑢 𝑦 ∈ 𝑤)
78		elpwi 4565	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ 𝒫 (fi‘𝑥) → 𝑢 ⊆ (fi‘𝑥))
79	78	sseld 3938	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ 𝒫 (fi‘𝑥) → (𝑤 ∈ 𝑢 → 𝑤 ∈ (fi‘𝑥)))
80	79	ad2antrl 740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑤 ∈ 𝑢 → 𝑤 ∈ (fi‘𝑥)))
81		elfi 9361	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑤 ∈ V ∧ 𝑥 ∈ V) → (𝑤 ∈ (fi‘𝑥) ↔ ∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = ∩ 𝑡))
82	81	el2v 3464	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ (fi‘𝑥) ↔ ∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = ∩ 𝑡)
83	80, 82	imbitrdi 254	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑤 ∈ 𝑢 → ∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = ∩ 𝑡))
84	2	alexsubALTlem3 24167	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)
85	78	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) → 𝑢 ⊆ (fi‘𝑥))
86	85	ad4antlr 745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑢 ⊆ (fi‘𝑥))
87		ssfii 9367	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥 ∈ V → 𝑥 ⊆ (fi‘𝑥))
88	87	elv 3462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑥 ⊆ (fi‘𝑥)
89		elinel1 4156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ 𝒫 𝑥)
90	89	elpwid 4567	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ⊆ 𝑥)
91	90	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) → 𝑡 ⊆ 𝑥)
92	91	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑡 ⊆ 𝑥)
93		simprl 782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑠 ∈ 𝑡)
94	92, 93	sseldd 3940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑠 ∈ 𝑥)
95	88, 94	sselid 3937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑠 ∈ (fi‘𝑥))
96	95	snssd 4748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → {𝑠} ⊆ (fi‘𝑥))
97	86, 96	unssd 4147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → (𝑢 ∪ {𝑠}) ⊆ (fi‘𝑥))
98		fvex 6884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (fi‘𝑥) ∈ V
99	98	elpw2 5295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑢 ∪ {𝑠}) ∈ 𝒫 (fi‘𝑥) ↔ (𝑢 ∪ {𝑠}) ⊆ (fi‘𝑥))
100	97, 99	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → (𝑢 ∪ {𝑠}) ∈ 𝒫 (fi‘𝑥))
101		simprl 782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) → 𝑎 ⊆ 𝑢)
102	101	ad4antlr 745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑎 ⊆ 𝑢)
103		ssun1 4133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 𝑢 ⊆ (𝑢 ∪ {𝑠})
104	102, 103	sstrdi 3951	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑎 ⊆ (𝑢 ∪ {𝑠}))
105		unieq 4879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑛 = 𝑏 → ∪ 𝑛 = ∪ 𝑏)
106	105	eqeq2d 2776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑛 = 𝑏 → (𝑋 = ∪ 𝑛 ↔ 𝑋 = ∪ 𝑏))
107	106	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 = 𝑏 → (¬ 𝑋 = ∪ 𝑛 ↔ ¬ 𝑋 = ∪ 𝑏))
108	107	cbvralvw 3243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛 ↔ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑏)
109	108	biimpi 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛 → ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑏)
110	109	ad2antll 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑏)
111	100, 104, 110	jca32 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → ((𝑢 ∪ {𝑠}) ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ (𝑢 ∪ {𝑠}) ∧ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
112		sseq2 3965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = (𝑢 ∪ {𝑠}) → (𝑎 ⊆ 𝑧 ↔ 𝑎 ⊆ (𝑢 ∪ {𝑠})))
113		pweq 4572	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 = (𝑢 ∪ {𝑠}) → 𝒫 𝑧 = 𝒫 (𝑢 ∪ {𝑠}))
114	113	ineq1d 4174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 = (𝑢 ∪ {𝑠}) → (𝒫 𝑧 ∩ Fin) = (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin))
115	114	raleqdv 3323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = (𝑢 ∪ {𝑠}) → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 ↔ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑏))
116	112, 115	anbi12d 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = (𝑢 ∪ {𝑠}) → ((𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ↔ (𝑎 ⊆ (𝑢 ∪ {𝑠}) ∧ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
117	116	elrab 3653	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑢 ∪ {𝑠}) ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ↔ ((𝑢 ∪ {𝑠}) ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ (𝑢 ∪ {𝑠}) ∧ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
118	111, 117	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → (𝑢 ∪ {𝑠}) ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)})
119		elun1 4137	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑢 ∪ {𝑠}) ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} → (𝑢 ∪ {𝑠}) ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}))
120	118, 119	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → (𝑢 ∪ {𝑠}) ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}))
121		vsnid 4625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑠 ∈ {𝑠}
122		elun2 4138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑠 ∈ {𝑠} → 𝑠 ∈ (𝑢 ∪ {𝑠}))
123	121, 122	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝑠 ∈ (𝑢 ∪ {𝑠})
124		intss1 4924	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑠 ∈ 𝑡 → ∩ 𝑡 ⊆ 𝑠)
125		sseq1 3964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑤 = ∩ 𝑡 → (𝑤 ⊆ 𝑠 ↔ ∩ 𝑡 ⊆ 𝑠))
126	124, 125	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑠 ∈ 𝑡 → (𝑤 = ∩ 𝑡 → 𝑤 ⊆ 𝑠))
127	126	impcom 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑤 = ∩ 𝑡 ∧ 𝑠 ∈ 𝑡) → 𝑤 ⊆ 𝑠)
128	127	ad4ant24 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ 𝑠 ∈ 𝑡) → 𝑤 ⊆ 𝑠)
129	128	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑤 ∈ 𝑢 ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ 𝑠 ∈ 𝑡)) → 𝑤 ⊆ 𝑠)
130	129	adantrrr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑤 ∈ 𝑢 ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → 𝑤 ⊆ 𝑠)
131	130	adantll 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → 𝑤 ⊆ 𝑠)
132		simprlr 791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → 𝑦 ∈ 𝑤)
133	131, 132	sseldd 3940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → 𝑦 ∈ 𝑠)
134	90	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) → 𝑡 ⊆ 𝑥)
135	134	ad2antrl 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → 𝑡 ⊆ 𝑥)
136		simprrl 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → 𝑠 ∈ 𝑡)
137	135, 136	sseldd 3940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → 𝑠 ∈ 𝑥)
138		elin 3923	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑠 ∈ (𝑥 ∩ 𝑢) ↔ (𝑠 ∈ 𝑥 ∧ 𝑠 ∈ 𝑢))
139		elunii 4873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑦 ∈ 𝑠 ∧ 𝑠 ∈ (𝑥 ∩ 𝑢)) → 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))
140	139	ex 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑦 ∈ 𝑠 → (𝑠 ∈ (𝑥 ∩ 𝑢) → 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))
141	138, 140	biimtrrid 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑦 ∈ 𝑠 → ((𝑠 ∈ 𝑥 ∧ 𝑠 ∈ 𝑢) → 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))
142	141	expd 420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 ∈ 𝑠 → (𝑠 ∈ 𝑥 → (𝑠 ∈ 𝑢 → 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))))
143	133, 137, 142	sylc 66	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → (𝑠 ∈ 𝑢 → 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))
144	143	con3d 153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ¬ 𝑠 ∈ 𝑢))
145	144	expr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤)) → ((𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛) → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ¬ 𝑠 ∈ 𝑢)))
146	145	com23 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤)) → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ((𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛) → ¬ 𝑠 ∈ 𝑢)))
147	146	exp32 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) → ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) → (𝑦 ∈ 𝑤 → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ((𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛) → ¬ 𝑠 ∈ 𝑢)))))
148	147	imp55 447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → ¬ 𝑠 ∈ 𝑢)
149		vex 3461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑠 ∈ V
150		eleq1w 2848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑣 = 𝑠 → (𝑣 ∈ (𝑢 ∪ {𝑠}) ↔ 𝑠 ∈ (𝑢 ∪ {𝑠})))
151		elequ1 2152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑣 = 𝑠 → (𝑣 ∈ 𝑢 ↔ 𝑠 ∈ 𝑢))
152	151	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑣 = 𝑠 → (¬ 𝑣 ∈ 𝑢 ↔ ¬ 𝑠 ∈ 𝑢))
153	150, 152	anbi12d 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑣 = 𝑠 → ((𝑣 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑣 ∈ 𝑢) ↔ (𝑠 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑠 ∈ 𝑢)))
154	149, 153	spcev 3568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑠 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑠 ∈ 𝑢) → ∃𝑣(𝑣 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑣 ∈ 𝑢))
155	123, 148, 154	sylancr 598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → ∃𝑣(𝑣 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑣 ∈ 𝑢))
156		nss 4003	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (¬ (𝑢 ∪ {𝑠}) ⊆ 𝑢 ↔ ∃𝑣(𝑣 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑣 ∈ 𝑢))
157	155, 156	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → ¬ (𝑢 ∪ {𝑠}) ⊆ 𝑢)
158		eqimss2 3998	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑢 = (𝑢 ∪ {𝑠}) → (𝑢 ∪ {𝑠}) ⊆ 𝑢)
159	158	necon3bi 2986	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (¬ (𝑢 ∪ {𝑠}) ⊆ 𝑢 → 𝑢 ≠ (𝑢 ∪ {𝑠}))
160	157, 159	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑢 ≠ (𝑢 ∪ {𝑠}))
161	160, 103	jctil 528	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → (𝑢 ⊆ (𝑢 ∪ {𝑠}) ∧ 𝑢 ≠ (𝑢 ∪ {𝑠})))
162		df-pss 3927	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 ⊊ (𝑢 ∪ {𝑠}) ↔ (𝑢 ⊆ (𝑢 ∪ {𝑠}) ∧ 𝑢 ≠ (𝑢 ∪ {𝑠})))
163	161, 162	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑢 ⊊ (𝑢 ∪ {𝑠}))
164		psseq2 4047	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑣 = (𝑢 ∪ {𝑠}) → (𝑢 ⊊ 𝑣 ↔ 𝑢 ⊊ (𝑢 ∪ {𝑠})))
165	164	rspcev 3584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑢 ∪ {𝑠}) ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧ 𝑢 ⊊ (𝑢 ∪ {𝑠})) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣)
166	120, 163, 165	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣)
167	84, 166	rexlimddv 3172	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣)
168	167	exp45 443	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) → ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) → (𝑦 ∈ 𝑤 → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣))))
169	168	expd 420	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) → (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → (𝑤 = ∩ 𝑡 → (𝑦 ∈ 𝑤 → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣)))))
170	169	rexlimdv 3164	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) → (∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = ∩ 𝑡 → (𝑦 ∈ 𝑤 → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣))))
171	170	ex 417	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑤 ∈ 𝑢 → (∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = ∩ 𝑡 → (𝑦 ∈ 𝑤 → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣)))))
172	83, 171	mpdd 44	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑤 ∈ 𝑢 → (𝑦 ∈ 𝑤 → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣))))
173	172	rexlimdv 3164	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (∃𝑤 ∈ 𝑢 𝑦 ∈ 𝑤 → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣)))
174	77, 173	biimtrid 245	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑦 ∈ ∪ 𝑢 → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣)))
175	174	rexlimdv 3164	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (∃𝑦 ∈ ∪ 𝑢 ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣))
176	76, 175	biimtrid 245	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (¬ ∪ 𝑢 ⊆ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣))
177	18, 73, 176	3syld 61	. . . . . . . . . . . . . 14 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑋 = ∪ 𝑎 → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣))
178	177	con3d 153	. . . . . . . . . . . . 13 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (¬ ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎))
179	14, 178	biimtrid 245	. . . . . . . . . . . 12 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎))
180	179	ex 417	. . . . . . . . . . 11 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎)))
181	180	adantr 485	. . . . . . . . . 10 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎)))
182		ssun1 4133	. . . . . . . . . . . . . 14 ⊢ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})
183		eqimss2 3998	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑎 → 𝑎 ⊆ 𝑧)
184	183	biantrurd 541	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑎 → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 ↔ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
185		pweq 4572	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑎 → 𝒫 𝑧 = 𝒫 𝑎)
186	185	ineq1d 4174	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑎 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑎 ∩ Fin))
187	186	raleqdv 3323	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑎 → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 ↔ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))
188	184, 187	bitr3d 284	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑎 → ((𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ↔ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))
189		simpll3 1231	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → 𝑎 ∈ 𝒫 (fi‘𝑥))
190		simplr 780	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)
191	188, 189, 190	elrabd 3655	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → 𝑎 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)})
192	182, 191	sselid 3937	. . . . . . . . . . . . 13 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → 𝑎 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}))
193		psseq2 4047	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑎 → (𝑢 ⊊ 𝑣 ↔ 𝑢 ⊊ 𝑎))
194	193	notbid 321	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑎 → (¬ 𝑢 ⊊ 𝑣 ↔ ¬ 𝑢 ⊊ 𝑎))
195	194	rspcv 3580	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑢 ⊊ 𝑎))
196	192, 195	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑢 ⊊ 𝑎))
197		id 23	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ∅ → 𝑎 = ∅)
198		0elpw 5317	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ 𝒫 𝑎
199		0fi 9027	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ Fin
200	198, 199	elini 4154	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ (𝒫 𝑎 ∩ Fin)
201	197, 200	eqeltrdi 2873	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ∅ → 𝑎 ∈ (𝒫 𝑎 ∩ Fin))
202		unieq 4879	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 𝑎 → ∪ 𝑏 = ∪ 𝑎)
203	202	eqeq2d 2776	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑎 → (𝑋 = ∪ 𝑏 ↔ 𝑋 = ∪ 𝑎))
204	203	notbid 321	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑎 → (¬ 𝑋 = ∪ 𝑏 ↔ ¬ 𝑋 = ∪ 𝑎))
205	204	rspccv 3581	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → (𝑎 ∈ (𝒫 𝑎 ∩ Fin) → ¬ 𝑋 = ∪ 𝑎))
206	201, 205	syl5 35	. . . . . . . . . . . . . . 15 ⊢ (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → (𝑎 = ∅ → ¬ 𝑋 = ∪ 𝑎))
207	206	necon2ad 2975	. . . . . . . . . . . . . 14 ⊢ (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → (𝑋 = ∪ 𝑎 → 𝑎 ≠ ∅))
208	207	ad2antlr 739	. . . . . . . . . . . . 13 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → (𝑋 = ∪ 𝑎 → 𝑎 ≠ ∅))
209		psseq1 4046	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = ∅ → (𝑢 ⊊ 𝑎 ↔ ∅ ⊊ 𝑎))
210	209	adantl 486	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → (𝑢 ⊊ 𝑎 ↔ ∅ ⊊ 𝑎))
211		0pss 4404	. . . . . . . . . . . . . 14 ⊢ (∅ ⊊ 𝑎 ↔ 𝑎 ≠ ∅)
212	210, 211	bitrdi 290	. . . . . . . . . . . . 13 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → (𝑢 ⊊ 𝑎 ↔ 𝑎 ≠ ∅))
213	208, 212	sylibrd 262	. . . . . . . . . . . 12 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → (𝑋 = ∪ 𝑎 → 𝑢 ⊊ 𝑎))
214	196, 213	nsyld 157	. . . . . . . . . . 11 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎))
215	214	ex 417	. . . . . . . . . 10 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → (𝑢 = ∅ → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎)))
216	181, 215	jaod 872	. . . . . . . . 9 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → (((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) ∨ 𝑢 = ∅) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎)))
217	13, 216	biimtrid 245	. . . . . . . 8 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → (𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎)))
218	217	rexlimdv 3164	. . . . . . 7 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → (∃𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎))
219	3, 218	mpd 16	. . . . . 6 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → ¬ 𝑋 = ∪ 𝑎)
220	219	ex 417	. . . . 5 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ 𝑎))
221	1, 220	biimtrrid 246	. . . 4 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (¬ ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ 𝑎))
222	221	con4d 116	. . 3 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
223	222	3exp 1135	. 2 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → (𝑎 ∈ 𝒫 (fi‘𝑥) → (𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))))
224	223	ralrimdv 3163	1 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → ∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∧ w3a 1101   = wceq 1563  ∃wex 1802   ∈ wcel 2145   ≠ wne 2960  ∀wral 3079  ∃wrex 3089  {crab 3417  Vcvv 3457   ∪ cun 3905   ∩ cin 3906   ⊆ wss 3907   ⊊ wpss 3908  ∅c0 4288  𝒫 cpw 4558  {csn 4585  ∪ cuni 4868  ∩ cint 4908  ‘cfv 6525  Fincfn 8931  ficfi 9358  topGenctg 17480  TopBasesctb 23063

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

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

This theorem is referenced by:  alexsubALT  24169