Theorem alexsubALTlem4 21854

Description: Lemma for alexsubALT 21855. 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 2992	. . . . 5 ⊢ (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 ↔ ¬ ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)
2		alexsubALT.1	. . . . . . . 8 ⊢ 𝑋 = ∪ 𝐽
3	2	alexsubALTlem2 21852	. . . . . . 7 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → ∃𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣)
4		elun 3753	. . . . . . . . . 10 ⊢ (𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ↔ (𝑢 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∨ 𝑢 ∈ {∅}))
5		sseq2 3627	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑢 → (𝑎 ⊆ 𝑧 ↔ 𝑎 ⊆ 𝑢))
6		pweq 4161	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑢 → 𝒫 𝑧 = 𝒫 𝑢)
7	6	ineq1d 3813	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑢 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑢 ∩ Fin))
8	7	raleqdv 3144	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑢 → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 ↔ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))
9	5, 8	anbi12d 747	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑢 → ((𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ↔ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
10	9	elrab 3363	. . . . . . . . . . 11 ⊢ (𝑢 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ↔ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
11		velsn 4193	. . . . . . . . . . 11 ⊢ (𝑢 ∈ {∅} ↔ 𝑢 = ∅)
12	10, 11	orbi12i 543	. . . . . . . . . 10 ⊢ ((𝑢 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∨ 𝑢 ∈ {∅}) ↔ ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) ∨ 𝑢 = ∅))
13	4, 12	bitri 264	. . . . . . . . 9 ⊢ (𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ↔ ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) ∨ 𝑢 = ∅))
14		ralnex 2992	. . . . . . . . . . . . 13 ⊢ (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 ↔ ¬ ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣)
15		simprrl 804	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → 𝑎 ⊆ 𝑢)
16	15	unissd 4462	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → ∪ 𝑎 ⊆ ∪ 𝑢)
17		sseq1 3626	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 = ∪ 𝑎 → (𝑋 ⊆ ∪ 𝑢 ↔ ∪ 𝑎 ⊆ ∪ 𝑢))
18	16, 17	syl5ibrcom 237	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑋 = ∪ 𝑎 → 𝑋 ⊆ ∪ 𝑢))
19		inss1 3833	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∩ 𝑢) ⊆ 𝑥
20		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 𝑥 ∈ V
21	20	elpw2 4828	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∩ 𝑢) ∈ 𝒫 𝑥 ↔ (𝑥 ∩ 𝑢) ⊆ 𝑥)
22	19, 21	mpbir 221	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∩ 𝑢) ∈ 𝒫 𝑥
23		unieq 4444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 = (𝑥 ∩ 𝑢) → ∪ 𝑐 = ∪ (𝑥 ∩ 𝑢))
24	23	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 = (𝑥 ∩ 𝑢) → (𝑋 = ∪ 𝑐 ↔ 𝑋 = ∪ (𝑥 ∩ 𝑢)))
25		pweq 4161	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑐 = (𝑥 ∩ 𝑢) → 𝒫 𝑐 = 𝒫 (𝑥 ∩ 𝑢))
26	25	ineq1d 3813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 = (𝑥 ∩ 𝑢) → (𝒫 𝑐 ∩ Fin) = (𝒫 (𝑥 ∩ 𝑢) ∩ Fin))
27	26	rexeqdv 3145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 = (𝑥 ∩ 𝑢) → (∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑 ↔ ∃𝑑 ∈ (𝒫 (𝑥 ∩ 𝑢) ∩ Fin)𝑋 = ∪ 𝑑))
28	24, 27	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 = (𝑥 ∩ 𝑢) → ((𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ↔ (𝑋 = ∪ (𝑥 ∩ 𝑢) → ∃𝑑 ∈ (𝒫 (𝑥 ∩ 𝑢) ∩ Fin)𝑋 = ∪ 𝑑)))
29	28	rspccv 3306	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → ((𝑥 ∩ 𝑢) ∈ 𝒫 𝑥 → (𝑋 = ∪ (𝑥 ∩ 𝑢) → ∃𝑑 ∈ (𝒫 (𝑥 ∩ 𝑢) ∩ Fin)𝑋 = ∪ 𝑑)))
30	22, 29	mpi 20	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → (𝑋 = ∪ (𝑥 ∩ 𝑢) → ∃𝑑 ∈ (𝒫 (𝑥 ∩ 𝑢) ∩ Fin)𝑋 = ∪ 𝑑))
31		inss2 3834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∩ 𝑢) ⊆ 𝑢
32		sstr 3611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑑 ⊆ (𝑥 ∩ 𝑢) ∧ (𝑥 ∩ 𝑢) ⊆ 𝑢) → 𝑑 ⊆ 𝑢)
33	31, 32	mpan2 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑑 ⊆ (𝑥 ∩ 𝑢) → 𝑑 ⊆ 𝑢)
34	33	anim1i 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑑 ⊆ (𝑥 ∩ 𝑢) ∧ 𝑑 ∈ Fin) → (𝑑 ⊆ 𝑢 ∧ 𝑑 ∈ Fin))
35		elfpw 8268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑑 ∈ (𝒫 (𝑥 ∩ 𝑢) ∩ Fin) ↔ (𝑑 ⊆ (𝑥 ∩ 𝑢) ∧ 𝑑 ∈ Fin))
36		elfpw 8268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑑 ∈ (𝒫 𝑢 ∩ Fin) ↔ (𝑑 ⊆ 𝑢 ∧ 𝑑 ∈ Fin))
37	34, 35, 36	3imtr4i 281	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑑 ∈ (𝒫 (𝑥 ∩ 𝑢) ∩ Fin) → 𝑑 ∈ (𝒫 𝑢 ∩ Fin))
38	37	anim1i 592	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑑 ∈ (𝒫 (𝑥 ∩ 𝑢) ∩ Fin) ∧ 𝑋 = ∪ 𝑑) → (𝑑 ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = ∪ 𝑑))
39	38	reximi2 3010	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑑 ∈ (𝒫 (𝑥 ∩ 𝑢) ∩ Fin)𝑋 = ∪ 𝑑 → ∃𝑑 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑑)
40	30, 39	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → (𝑋 = ∪ (𝑥 ∩ 𝑢) → ∃𝑑 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑑))
41		unieq 4444	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑑 = 𝑏 → ∪ 𝑑 = ∪ 𝑏)
42	41	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = 𝑏 → (𝑋 = ∪ 𝑑 ↔ 𝑋 = ∪ 𝑏))
43	42	cbvrexv 3172	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∃𝑑 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑑 ↔ ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏)
44	40, 43	syl6ib 241	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → (𝑋 = ∪ (𝑥 ∩ 𝑢) → ∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏))
45		dfrex2 2996	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃𝑏 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑏 ↔ ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)
46	44, 45	syl6ib 241	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → (𝑋 = ∪ (𝑥 ∩ 𝑢) → ¬ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))
47	46	con2d 129	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ (𝑥 ∩ 𝑢)))
48	47	a1d 25	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → (𝑎 ⊆ 𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ (𝑥 ∩ 𝑢))))
49	48	3ad2ant2 1083	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (𝑎 ⊆ 𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ (𝑥 ∩ 𝑢))))
50	49	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ 𝑢 ∈ 𝒫 (fi‘𝑥)) → (𝑎 ⊆ 𝑢 → (∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ (𝑥 ∩ 𝑢))))
51	50	impd 447	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ 𝑢 ∈ 𝒫 (fi‘𝑥)) → ((𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → ¬ 𝑋 = ∪ (𝑥 ∩ 𝑢)))
52	51	impr 649	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → ¬ 𝑋 = ∪ (𝑥 ∩ 𝑢))
53	19	unissi 4461	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ (𝑥 ∩ 𝑢) ⊆ ∪ 𝑥
54		unieq 4444	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → ∪ 𝐽 = ∪ (topGen‘(fi‘𝑥)))
55		fiuni 8334	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ V → ∪ 𝑥 = ∪ (fi‘𝑥))
56	20, 55	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ 𝑥 = ∪ (fi‘𝑥)
57		fibas 20781	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (fi‘𝑥) ∈ TopBases
58		unitg 20771	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((fi‘𝑥) ∈ TopBases → ∪ (topGen‘(fi‘𝑥)) = ∪ (fi‘𝑥))
59	57, 58	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ (topGen‘(fi‘𝑥)) = ∪ (fi‘𝑥)
60	56, 59	eqtr4i 2647	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∪ 𝑥 = ∪ (topGen‘(fi‘𝑥))
61	54, 60	syl6reqr 2675	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → ∪ 𝑥 = ∪ 𝐽)
62	61, 2	syl6eqr 2674	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → ∪ 𝑥 = 𝑋)
63	62	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → ∪ 𝑥 = 𝑋)
64	63	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → ∪ 𝑥 = 𝑋)
65	53, 64	syl5sseq 3653	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → ∪ (𝑥 ∩ 𝑢) ⊆ 𝑋)
66		eqcom 2629	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋 = ∪ (𝑥 ∩ 𝑢) ↔ ∪ (𝑥 ∩ 𝑢) = 𝑋)
67		eqss 3618	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∪ (𝑥 ∩ 𝑢) = 𝑋 ↔ (∪ (𝑥 ∩ 𝑢) ⊆ 𝑋 ∧ 𝑋 ⊆ ∪ (𝑥 ∩ 𝑢)))
68	67	baib 944	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ (𝑥 ∩ 𝑢) ⊆ 𝑋 → (∪ (𝑥 ∩ 𝑢) = 𝑋 ↔ 𝑋 ⊆ ∪ (𝑥 ∩ 𝑢)))
69	66, 68	syl5bb 272	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ (𝑥 ∩ 𝑢) ⊆ 𝑋 → (𝑋 = ∪ (𝑥 ∩ 𝑢) ↔ 𝑋 ⊆ ∪ (𝑥 ∩ 𝑢)))
70	65, 69	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑋 = ∪ (𝑥 ∩ 𝑢) ↔ 𝑋 ⊆ ∪ (𝑥 ∩ 𝑢)))
71	52, 70	mtbid 314	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → ¬ 𝑋 ⊆ ∪ (𝑥 ∩ 𝑢))
72		sstr2 3610	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ⊆ ∪ 𝑢 → (∪ 𝑢 ⊆ ∪ (𝑥 ∩ 𝑢) → 𝑋 ⊆ ∪ (𝑥 ∩ 𝑢)))
73	72	con3rr3 151	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑋 ⊆ ∪ (𝑥 ∩ 𝑢) → (𝑋 ⊆ ∪ 𝑢 → ¬ ∪ 𝑢 ⊆ ∪ (𝑥 ∩ 𝑢)))
74	71, 73	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑋 ⊆ ∪ 𝑢 → ¬ ∪ 𝑢 ⊆ ∪ (𝑥 ∩ 𝑢)))
75		nss 3663	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ∪ 𝑢 ⊆ ∪ (𝑥 ∩ 𝑢) ↔ ∃𝑦(𝑦 ∈ ∪ 𝑢 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))
76		df-rex 2918	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑦 ∈ ∪ 𝑢 ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) ↔ ∃𝑦(𝑦 ∈ ∪ 𝑢 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))
77	75, 76	bitr4i 267	. . . . . . . . . . . . . . . 16 ⊢ (¬ ∪ 𝑢 ⊆ ∪ (𝑥 ∩ 𝑢) ↔ ∃𝑦 ∈ ∪ 𝑢 ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))
78		eluni2 4440	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ∪ 𝑢 ↔ ∃𝑤 ∈ 𝑢 𝑦 ∈ 𝑤)
79		elpwi 4168	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ 𝒫 (fi‘𝑥) → 𝑢 ⊆ (fi‘𝑥))
80	79	sseld 3602	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ 𝒫 (fi‘𝑥) → (𝑤 ∈ 𝑢 → 𝑤 ∈ (fi‘𝑥)))
81	80	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑤 ∈ 𝑢 → 𝑤 ∈ (fi‘𝑥)))
82		vex 3203	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑤 ∈ V
83		elfi 8319	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑤 ∈ V ∧ 𝑥 ∈ V) → (𝑤 ∈ (fi‘𝑥) ↔ ∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = ∩ 𝑡))
84	82, 20, 83	mp2an 708	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ (fi‘𝑥) ↔ ∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = ∩ 𝑡)
85	81, 84	syl6ib 241	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑤 ∈ 𝑢 → ∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = ∩ 𝑡))
86	2	alexsubALTlem3 21853	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)
87	79	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) → 𝑢 ⊆ (fi‘𝑥))
88	87	ad4antlr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑢 ⊆ (fi‘𝑥))
89		ssfii 8325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥 ∈ V → 𝑥 ⊆ (fi‘𝑥))
90	20, 89	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑥 ⊆ (fi‘𝑥)
91		inss1 3833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝒫 𝑥 ∩ Fin) ⊆ 𝒫 𝑥
92	91	sseli 3599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ∈ 𝒫 𝑥)
93	92	elpwid 4170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → 𝑡 ⊆ 𝑥)
94	93	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))) → 𝑡 ⊆ 𝑥)
95	94	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑡 ⊆ 𝑥)
96		simprl 794	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑠 ∈ 𝑡)
97	95, 96	sseldd 3604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑠 ∈ 𝑥)
98	90, 97	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑠 ∈ (fi‘𝑥))
99	98	snssd 4340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → {𝑠} ⊆ (fi‘𝑥))
100	88, 99	unssd 3789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → (𝑢 ∪ {𝑠}) ⊆ (fi‘𝑥))
101		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (fi‘𝑥) ∈ V
102	101	elpw2 4828	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑢 ∪ {𝑠}) ∈ 𝒫 (fi‘𝑥) ↔ (𝑢 ∪ {𝑠}) ⊆ (fi‘𝑥))
103	100, 102	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → (𝑢 ∪ {𝑠}) ∈ 𝒫 (fi‘𝑥))
104		simprl 794	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) → 𝑎 ⊆ 𝑢)
105	104	ad4antlr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑎 ⊆ 𝑢)
106		ssun1 3776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 𝑢 ⊆ (𝑢 ∪ {𝑠})
107	105, 106	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑎 ⊆ (𝑢 ∪ {𝑠}))
108		unieq 4444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑛 = 𝑏 → ∪ 𝑛 = ∪ 𝑏)
109	108	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑛 = 𝑏 → (𝑋 = ∪ 𝑛 ↔ 𝑋 = ∪ 𝑏))
110	109	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 = 𝑏 → (¬ 𝑋 = ∪ 𝑛 ↔ ¬ 𝑋 = ∪ 𝑏))
111	110	cbvralv 3171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛 ↔ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑏)
112	111	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛 → ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑏)
113	112	ad2antll 765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑏)
114	103, 107, 113	jca32 558	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → ((𝑢 ∪ {𝑠}) ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ (𝑢 ∪ {𝑠}) ∧ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
115		sseq2 3627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = (𝑢 ∪ {𝑠}) → (𝑎 ⊆ 𝑧 ↔ 𝑎 ⊆ (𝑢 ∪ {𝑠})))
116		pweq 4161	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 = (𝑢 ∪ {𝑠}) → 𝒫 𝑧 = 𝒫 (𝑢 ∪ {𝑠}))
117	116	ineq1d 3813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 = (𝑢 ∪ {𝑠}) → (𝒫 𝑧 ∩ Fin) = (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin))
118	117	raleqdv 3144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = (𝑢 ∪ {𝑠}) → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 ↔ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑏))
119	115, 118	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = (𝑢 ∪ {𝑠}) → ((𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ↔ (𝑎 ⊆ (𝑢 ∪ {𝑠}) ∧ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
120	119	elrab 3363	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑢 ∪ {𝑠}) ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ↔ ((𝑢 ∪ {𝑠}) ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ (𝑢 ∪ {𝑠}) ∧ ∀𝑏 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
121	114, 120	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → (𝑢 ∪ {𝑠}) ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)})
122		elun1 3780	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑢 ∪ {𝑠}) ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} → (𝑢 ∪ {𝑠}) ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}))
123	121, 122	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → (𝑢 ∪ {𝑠}) ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}))
124		vsnid 4209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑠 ∈ {𝑠}
125		elun2 3781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑠 ∈ {𝑠} → 𝑠 ∈ (𝑢 ∪ {𝑠}))
126	124, 125	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝑠 ∈ (𝑢 ∪ {𝑠})
127		intss1 4492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑠 ∈ 𝑡 → ∩ 𝑡 ⊆ 𝑠)
128		sseq1 3626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑤 = ∩ 𝑡 → (𝑤 ⊆ 𝑠 ↔ ∩ 𝑡 ⊆ 𝑠))
129	127, 128	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑠 ∈ 𝑡 → (𝑤 = ∩ 𝑡 → 𝑤 ⊆ 𝑠))
130	129	impcom 446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑤 = ∩ 𝑡 ∧ 𝑠 ∈ 𝑡) → 𝑤 ⊆ 𝑠)
131	130	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑠 ∈ 𝑡) → 𝑤 ⊆ 𝑠)
132	131	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ 𝑠 ∈ 𝑡) → 𝑤 ⊆ 𝑠)
133	132	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑤 ∈ 𝑢 ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ 𝑠 ∈ 𝑡)) → 𝑤 ⊆ 𝑠)
134	133	adantrrr 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑤 ∈ 𝑢 ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → 𝑤 ⊆ 𝑠)
135	134	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → 𝑤 ⊆ 𝑠)
136		simprlr 803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → 𝑦 ∈ 𝑤)
137	135, 136	sseldd 3604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → 𝑦 ∈ 𝑠)
138	93	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) → 𝑡 ⊆ 𝑥)
139	138	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → 𝑡 ⊆ 𝑥)
140		simprrl 804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → 𝑠 ∈ 𝑡)
141	139, 140	sseldd 3604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → 𝑠 ∈ 𝑥)
142		elin 3796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑠 ∈ (𝑥 ∩ 𝑢) ↔ (𝑠 ∈ 𝑥 ∧ 𝑠 ∈ 𝑢))
143		elunii 4441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑦 ∈ 𝑠 ∧ 𝑠 ∈ (𝑥 ∩ 𝑢)) → 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))
144	143	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑦 ∈ 𝑠 → (𝑠 ∈ (𝑥 ∩ 𝑢) → 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))
145	142, 144	syl5bir 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑦 ∈ 𝑠 → ((𝑠 ∈ 𝑥 ∧ 𝑠 ∈ 𝑢) → 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))
146	145	expd 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 ∈ 𝑠 → (𝑠 ∈ 𝑥 → (𝑠 ∈ 𝑢 → 𝑦 ∈ ∪ (𝑥 ∩ 𝑢))))
147	137, 141, 146	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → (𝑠 ∈ 𝑢 → 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))
148	147	con3d 148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ (((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛))) → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ¬ 𝑠 ∈ 𝑢))
149	148	expr 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤)) → ((𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛) → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ¬ 𝑠 ∈ 𝑢)))
150	149	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ 𝑦 ∈ 𝑤)) → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ((𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛) → ¬ 𝑠 ∈ 𝑢)))
151	150	exp32 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) → ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) → (𝑦 ∈ 𝑤 → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ((𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛) → ¬ 𝑠 ∈ 𝑢)))))
152	151	imp55 627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → ¬ 𝑠 ∈ 𝑢)
153		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑠 ∈ V
154		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑣 = 𝑠 → (𝑣 ∈ (𝑢 ∪ {𝑠}) ↔ 𝑠 ∈ (𝑢 ∪ {𝑠})))
155		elequ1 1997	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑣 = 𝑠 → (𝑣 ∈ 𝑢 ↔ 𝑠 ∈ 𝑢))
156	155	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑣 = 𝑠 → (¬ 𝑣 ∈ 𝑢 ↔ ¬ 𝑠 ∈ 𝑢))
157	154, 156	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑣 = 𝑠 → ((𝑣 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑣 ∈ 𝑢) ↔ (𝑠 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑠 ∈ 𝑢)))
158	153, 157	spcev 3300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑠 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑠 ∈ 𝑢) → ∃𝑣(𝑣 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑣 ∈ 𝑢))
159	126, 152, 158	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → ∃𝑣(𝑣 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑣 ∈ 𝑢))
160		nss 3663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (¬ (𝑢 ∪ {𝑠}) ⊆ 𝑢 ↔ ∃𝑣(𝑣 ∈ (𝑢 ∪ {𝑠}) ∧ ¬ 𝑣 ∈ 𝑢))
161	159, 160	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → ¬ (𝑢 ∪ {𝑠}) ⊆ 𝑢)
162		eqimss2 3658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑢 = (𝑢 ∪ {𝑠}) → (𝑢 ∪ {𝑠}) ⊆ 𝑢)
163	162	necon3bi 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (¬ (𝑢 ∪ {𝑠}) ⊆ 𝑢 → 𝑢 ≠ (𝑢 ∪ {𝑠}))
164	161, 163	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑢 ≠ (𝑢 ∪ {𝑠}))
165	164, 106	jctil 560	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → (𝑢 ⊆ (𝑢 ∪ {𝑠}) ∧ 𝑢 ≠ (𝑢 ∪ {𝑠})))
166		df-pss 3590	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 ⊊ (𝑢 ∪ {𝑠}) ↔ (𝑢 ⊆ (𝑢 ∪ {𝑠}) ∧ 𝑢 ≠ (𝑢 ∪ {𝑠})))
167	165, 166	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → 𝑢 ⊊ (𝑢 ∪ {𝑠}))
168		psseq2 3695	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑣 = (𝑢 ∪ {𝑠}) → (𝑢 ⊊ 𝑣 ↔ 𝑢 ⊊ (𝑢 ∪ {𝑠})))
169	168	rspcev 3309	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑢 ∪ {𝑠}) ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ∧ 𝑢 ⊊ (𝑢 ∪ {𝑠})) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣)
170	123, 167, 169	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) ∧ (𝑠 ∈ 𝑡 ∧ ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣)
171	86, 170	rexlimddv 3035	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣)
172	171	exp45 642	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) → ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) → (𝑦 ∈ 𝑤 → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣))))
173	172	expd 452	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) → (𝑡 ∈ (𝒫 𝑥 ∩ Fin) → (𝑤 = ∩ 𝑡 → (𝑦 ∈ 𝑤 → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣)))))
174	173	rexlimdv 3030	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) → (∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = ∩ 𝑡 → (𝑦 ∈ 𝑤 → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣))))
175	174	ex 450	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑤 ∈ 𝑢 → (∃𝑡 ∈ (𝒫 𝑥 ∩ Fin)𝑤 = ∩ 𝑡 → (𝑦 ∈ 𝑤 → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣)))))
176	85, 175	mpdd 43	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑤 ∈ 𝑢 → (𝑦 ∈ 𝑤 → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣))))
177	176	rexlimdv 3030	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (∃𝑤 ∈ 𝑢 𝑦 ∈ 𝑤 → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣)))
178	78, 177	syl5bi 232	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑦 ∈ ∪ 𝑢 → (¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣)))
179	178	rexlimdv 3030	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (∃𝑦 ∈ ∪ 𝑢 ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣))
180	77, 179	syl5bi 232	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (¬ ∪ 𝑢 ⊆ ∪ (𝑥 ∩ 𝑢) → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣))
181	18, 74, 180	3syld 60	. . . . . . . . . . . . . 14 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (𝑋 = ∪ 𝑎 → ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣))
182	181	con3d 148	. . . . . . . . . . . . 13 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (¬ ∃𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎))
183	14, 182	syl5bi 232	. . . . . . . . . . . 12 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎))
184	183	ex 450	. . . . . . . . . . 11 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎)))
185	184	adantr 481	. . . . . . . . . 10 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → ((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎)))
186		ssun1 3776	. . . . . . . . . . . . . 14 ⊢ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ⊆ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})
187		simpll3 1102	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → 𝑎 ∈ 𝒫 (fi‘𝑥))
188		simplr 792	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)
189		eqimss2 3658	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑎 → 𝑎 ⊆ 𝑧)
190	189	biantrurd 529	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑎 → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 ↔ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)))
191		pweq 4161	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑎 → 𝒫 𝑧 = 𝒫 𝑎)
192	191	ineq1d 3813	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑎 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑎 ∩ Fin))
193	192	raleqdv 3144	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑎 → (∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 ↔ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))
194	190, 193	bitr3d 270	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑎 → ((𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ↔ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))
195	194	elrab 3363	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ↔ (𝑎 ∈ 𝒫 (fi‘𝑥) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))
196	187, 188, 195	sylanbrc 698	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → 𝑎 ∈ {𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)})
197	186, 196	sseldi 3601	. . . . . . . . . . . . 13 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → 𝑎 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}))
198		psseq2 3695	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑎 → (𝑢 ⊊ 𝑣 ↔ 𝑢 ⊊ 𝑎))
199	198	notbid 308	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑎 → (¬ 𝑢 ⊊ 𝑣 ↔ ¬ 𝑢 ⊊ 𝑎))
200	199	rspcv 3305	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑢 ⊊ 𝑎))
201	197, 200	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑢 ⊊ 𝑎))
202		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ∅ → 𝑎 = ∅)
203		0elpw 4834	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ 𝒫 𝑎
204		0fin 8188	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ Fin
205		elin 3796	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ ∈ (𝒫 𝑎 ∩ Fin) ↔ (∅ ∈ 𝒫 𝑎 ∧ ∅ ∈ Fin))
206	203, 204, 205	mpbir2an 955	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ (𝒫 𝑎 ∩ Fin)
207	202, 206	syl6eqel 2709	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ∅ → 𝑎 ∈ (𝒫 𝑎 ∩ Fin))
208		unieq 4444	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 𝑎 → ∪ 𝑏 = ∪ 𝑎)
209	208	eqeq2d 2632	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑎 → (𝑋 = ∪ 𝑏 ↔ 𝑋 = ∪ 𝑎))
210	209	notbid 308	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑎 → (¬ 𝑋 = ∪ 𝑏 ↔ ¬ 𝑋 = ∪ 𝑎))
211	210	rspccv 3306	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → (𝑎 ∈ (𝒫 𝑎 ∩ Fin) → ¬ 𝑋 = ∪ 𝑎))
212	207, 211	syl5 34	. . . . . . . . . . . . . . 15 ⊢ (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → (𝑎 = ∅ → ¬ 𝑋 = ∪ 𝑎))
213	212	necon2ad 2809	. . . . . . . . . . . . . 14 ⊢ (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → (𝑋 = ∪ 𝑎 → 𝑎 ≠ ∅))
214	213	ad2antlr 763	. . . . . . . . . . . . 13 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → (𝑋 = ∪ 𝑎 → 𝑎 ≠ ∅))
215		psseq1 3694	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = ∅ → (𝑢 ⊊ 𝑎 ↔ ∅ ⊊ 𝑎))
216	215	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → (𝑢 ⊊ 𝑎 ↔ ∅ ⊊ 𝑎))
217		0pss 4013	. . . . . . . . . . . . . 14 ⊢ (∅ ⊊ 𝑎 ↔ 𝑎 ≠ ∅)
218	216, 217	syl6bb 276	. . . . . . . . . . . . 13 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → (𝑢 ⊊ 𝑎 ↔ 𝑎 ≠ ∅))
219	214, 218	sylibrd 249	. . . . . . . . . . . 12 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → (𝑋 = ∪ 𝑎 → 𝑢 ⊊ 𝑎))
220	201, 219	nsyld 154	. . . . . . . . . . 11 ⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) ∧ 𝑢 = ∅) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎))
221	220	ex 450	. . . . . . . . . 10 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → (𝑢 = ∅ → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎)))
222	185, 221	jaod 395	. . . . . . . . 9 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → (((𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)) ∨ 𝑢 = ∅) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎)))
223	13, 222	syl5bi 232	. . . . . . . 8 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → (𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) → (∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎)))
224	223	rexlimdv 3030	. . . . . . 7 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → (∃𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎))
225	3, 224	mpd 15	. . . . . 6 ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → ¬ 𝑋 = ∪ 𝑎)
226	225	ex 450	. . . . 5 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ 𝑎))
227	1, 226	syl5bir 233	. . . 4 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (¬ ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ 𝑎))
228	227	con4d 114	. . 3 ⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) → (𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
229	228	3exp 1264	. 2 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → (𝑎 ∈ 𝒫 (fi‘𝑥) → (𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))))
230	229	ralrimdv 2968	1 ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → ∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   ∧ w3a 1037   = wceq 1483  ∃wex 1704   ∈ wcel 1990   ≠ wne 2794  ∀wral 2912  ∃wrex 2913  {crab 2916  Vcvv 3200   ∪ cun 3572   ∩ cin 3573   ⊆ wss 3574   ⊊ wpss 3575  ∅c0 3915  𝒫 cpw 4158  {csn 4177  ∪ cuni 4436  ∩ cint 4475  ‘cfv 5888  Fincfn 7955  ficfi 8316  topGenctg 16098  TopBasesctb 20749

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-ac2 9285

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-rpss 6937  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-en 7956  df-fin 7959  df-fi 8317  df-card 8765  df-ac 8939  df-topgen 16104  df-bases 20750

This theorem is referenced by:  alexsubALT  21855