fiuncmp - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fiuncmp		Structured version Visualization version GIF version

Theorem fiuncmp 22157

Description: A finite union of compact sets is compact. (Contributed by Mario Carneiro, 19-Mar-2015.)

**Hypothesis**
Ref	Expression
fiuncmp.1	⊢ 𝑋 = ∪ 𝐽

**Assertion**
Ref	Expression
fiuncmp	⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp)

Distinct variable groups: 𝑥,𝐴 𝑥,𝐽 Allowed substitution hints: 𝐵(𝑥) 𝑋(𝑥)

Proof of Theorem fiuncmp Dummy variables 𝑡 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssid 3899	. 2 ⊢ 𝐴 ⊆ 𝐴
2		simp2 1138	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → 𝐴 ∈ Fin)
3		sseq1 3902	. . . . . 6 ⊢ (𝑡 = ∅ → (𝑡 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴))
4		iuneq1 4897	. . . . . . . . 9 ⊢ (𝑡 = ∅ → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ ∅ 𝐵)
5		0iun 4948	. . . . . . . . 9 ⊢ ∪ 𝑥 ∈ ∅ 𝐵 = ∅
6	4, 5	eqtrdi 2789	. . . . . . . 8 ⊢ (𝑡 = ∅ → ∪ 𝑥 ∈ 𝑡 𝐵 = ∅)
7	6	oveq2d 7188	. . . . . . 7 ⊢ (𝑡 = ∅ → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾_t ∅))
8	7	eleq1d 2817	. . . . . 6 ⊢ (𝑡 = ∅ → ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾_t ∅) ∈ Comp))
9	3, 8	imbi12d 348	. . . . 5 ⊢ (𝑡 = ∅ → ((𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ (∅ ⊆ 𝐴 → (𝐽 ↾_t ∅) ∈ Comp)))
10	9	imbi2d 344	. . . 4 ⊢ (𝑡 = ∅ → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (∅ ⊆ 𝐴 → (𝐽 ↾_t ∅) ∈ Comp))))
11		sseq1 3902	. . . . . 6 ⊢ (𝑡 = 𝑦 → (𝑡 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴))
12		iuneq1 4897	. . . . . . . 8 ⊢ (𝑡 = 𝑦 → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ 𝑦 𝐵)
13	12	oveq2d 7188	. . . . . . 7 ⊢ (𝑡 = 𝑦 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵))
14	13	eleq1d 2817	. . . . . 6 ⊢ (𝑡 = 𝑦 → ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp))
15	11, 14	imbi12d 348	. . . . 5 ⊢ (𝑡 = 𝑦 → ((𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ (𝑦 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)))
16	15	imbi2d 344	. . . 4 ⊢ (𝑡 = 𝑦 → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑦 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp))))
17		sseq1 3902	. . . . . 6 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → (𝑡 ⊆ 𝐴 ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐴))
18		iuneq1 4897	. . . . . . . 8 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
19	18	oveq2d 7188	. . . . . . 7 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵))
20	19	eleq1d 2817	. . . . . 6 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp))
21	17, 20	imbi12d 348	. . . . 5 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → ((𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)))
22	21	imbi2d 344	. . . 4 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp))))
23		sseq1 3902	. . . . . 6 ⊢ (𝑡 = 𝐴 → (𝑡 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴))
24		iuneq1 4897	. . . . . . . 8 ⊢ (𝑡 = 𝐴 → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵)
25	24	oveq2d 7188	. . . . . . 7 ⊢ (𝑡 = 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵))
26	25	eleq1d 2817	. . . . . 6 ⊢ (𝑡 = 𝐴 → ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp))
27	23, 26	imbi12d 348	. . . . 5 ⊢ (𝑡 = 𝐴 → ((𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ (𝐴 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp)))
28	27	imbi2d 344	. . . 4 ⊢ (𝑡 = 𝐴 → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝐴 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp))))
29		rest0 21922	. . . . . . 7 ⊢ (𝐽 ∈ Top → (𝐽 ↾_t ∅) = {∅})
30		0cmp 22147	. . . . . . 7 ⊢ {∅} ∈ Comp
31	29, 30	eqeltrdi 2841	. . . . . 6 ⊢ (𝐽 ∈ Top → (𝐽 ↾_t ∅) ∈ Comp)
32	31	3ad2ant1 1134	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝐽 ↾_t ∅) ∈ Comp)
33	32	a1d 25	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (∅ ⊆ 𝐴 → (𝐽 ↾_t ∅) ∈ Comp))
34		ssun1 4062	. . . . . . . . 9 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧})
35		id 22	. . . . . . . . 9 ⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
36	34, 35	sstrid 3888	. . . . . . . 8 ⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → 𝑦 ⊆ 𝐴)
37	36	imim1i 63	. . . . . . 7 ⊢ ((𝑦 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp))
38		simpl1 1192	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → 𝐽 ∈ Top)
39		iunxun 4979	. . . . . . . . . . . 12 ⊢ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 = (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵)
40		simprr 773	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)
41		cmptop 22148	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Top)
42		restrcl 21910	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Top → (𝐽 ∈ V ∧ ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V))
43	42	simprd 499	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Top → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V)
44	40, 41, 43	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V)
45		nfcv 2899	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡𝐵
46		nfcsb1v 3814	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥⦋𝑡 / 𝑥⦌𝐵
47		csbeq1a 3804	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑡 → 𝐵 = ⦋𝑡 / 𝑥⦌𝐵)
48	45, 46, 47	cbviun 4922	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑥 ∈ {𝑧}𝐵 = ∪ 𝑡 ∈ {𝑧}⦋𝑡 / 𝑥⦌𝐵
49		vex 3402	. . . . . . . . . . . . . . . 16 ⊢ 𝑧 ∈ V
50		csbeq1 3793	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑧 → ⦋𝑡 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵)
51	49, 50	iunxsn 4976	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑡 ∈ {𝑧}⦋𝑡 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵
52	48, 51	eqtri 2761	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑥 ∈ {𝑧}𝐵 = ⦋𝑧 / 𝑥⦌𝐵
53	50	oveq2d 7188	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑧 → (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) = (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵))
54	53	eleq1d 2817	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑧 → ((𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp ↔ (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Comp))
55		simpl3 1194	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp)
56		nfv 1921	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡(𝐽 ↾_t 𝐵) ∈ Comp
57		nfcv 2899	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥𝐽
58		nfcv 2899	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥 ↾_t
59	57, 58, 46	nfov 7202	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵)
60	59	nfel1 2915	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥(𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp
61	47	oveq2d 7188	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑡 → (𝐽 ↾_t 𝐵) = (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵))
62	61	eleq1d 2817	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑡 → ((𝐽 ↾_t 𝐵) ∈ Comp ↔ (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp))
63	56, 60, 62	cbvralw 3340	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp ↔ ∀𝑡 ∈ 𝐴 (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp)
64	55, 63	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∀𝑡 ∈ 𝐴 (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp)
65		ssun2 4063	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑧} ⊆ (𝑦 ∪ {𝑧})
66		simprl 771	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
67	65, 66	sstrid 3888	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → {𝑧} ⊆ 𝐴)
68	49	snss 4674	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝐴 ↔ {𝑧} ⊆ 𝐴)
69	67, 68	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → 𝑧 ∈ 𝐴)
70	54, 64, 69	rspcdva 3528	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Comp)
71		cmptop 22148	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Comp → (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Top)
72		restrcl 21910	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Top → (𝐽 ∈ V ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ V))
73	72	simprd 499	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Top → ⦋𝑧 / 𝑥⦌𝐵 ∈ V)
74	70, 71, 73	3syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ⦋𝑧 / 𝑥⦌𝐵 ∈ V)
75	52, 74	eqeltrid 2837	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ 𝑥 ∈ {𝑧}𝐵 ∈ V)
76		unexg 7492	. . . . . . . . . . . . 13 ⊢ ((∪ 𝑥 ∈ 𝑦 𝐵 ∈ V ∧ ∪ 𝑥 ∈ {𝑧}𝐵 ∈ V) → (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵) ∈ V)
77	44, 75, 76	syl2anc 587	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵) ∈ V)
78	39, 77	eqeltrid 2837	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V)
79		resttop 21913	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Top)
80	38, 78, 79	syl2anc 587	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Top)
81		eqid 2738	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝐽 = ∪ 𝐽
82	81	restin 21919	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
83	38, 78, 82	syl2anc 587	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
84	83	unieqd 4810	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ∪ (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
85		inss2 4120	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝐽
86		fiuncmp.1	. . . . . . . . . . . . . 14 ⊢ 𝑋 = ∪ 𝐽
87	85, 86	sseqtrri 3914	. . . . . . . . . . . . 13 ⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) ⊆ 𝑋
88	86	restuni 21915	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) ⊆ 𝑋) → (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ∪ (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
89	38, 87, 88	sylancl 589	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ∪ (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
90	84, 89	eqtr4d 2776	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽))
91	52	uneq2i 4050	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵) = (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵)
92	39, 91	eqtri 2761	. . . . . . . . . . . . 13 ⊢ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 = (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵)
93	92	ineq1i 4099	. . . . . . . . . . . 12 ⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵) ∩ ∪ 𝐽)
94		indir 4166	. . . . . . . . . . . 12 ⊢ ((∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵) ∩ ∪ 𝐽) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))
95	93, 94	eqtri 2761	. . . . . . . . . . 11 ⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))
96	90, 95	eqtrdi 2789	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
97		inss1 4119	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ 𝑦 𝐵
98		ssun1 4062	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵)
99	98, 39	sseqtrri 3914	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
100	97, 99	sstri 3886	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
101	100	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
102		restabs 21918	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)))
103	38, 101, 78, 102	syl3anc 1372	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)))
104	81	restin 21919	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V) → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) = (𝐽 ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)))
105	38, 44, 104	syl2anc 587	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) = (𝐽 ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)))
106	103, 105	eqtr4d 2776	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵))
107	106, 40	eqeltrd 2833	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) ∈ Comp)
108		inss1 4119	. . . . . . . . . . . . . . 15 ⊢ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ⦋𝑧 / 𝑥⦌𝐵
109		ssun2 4063	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑥 ∈ {𝑧}𝐵 ⊆ (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵)
110	109, 39	sseqtrri 3914	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑥 ∈ {𝑧}𝐵 ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
111	52, 110	eqsstrri 3912	. . . . . . . . . . . . . . 15 ⊢ ⦋𝑧 / 𝑥⦌𝐵 ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
112	108, 111	sstri 3886	. . . . . . . . . . . . . 14 ⊢ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
113	112	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
114		restabs 21918	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
115	38, 113, 78, 114	syl3anc 1372	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
116	81	restin 21919	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ V) → (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) = (𝐽 ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
117	38, 74, 116	syl2anc 587	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) = (𝐽 ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
118	115, 117	eqtr4d 2776	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵))
119	118, 70	eqeltrd 2833	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) ∈ Comp)
120		eqid 2738	. . . . . . . . . . 11 ⊢ ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
121	120	uncmp 22156	. . . . . . . . . 10 ⊢ ((((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Top ∧ ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))) ∧ (((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) ∈ Comp ∧ ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)
122	80, 96, 107, 119, 121	syl22anc 838	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)
123	122	exp32 424	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)))
124	123	a2d 29	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)))
125	37, 124	syl5 34	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → ((𝑦 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)))
126	125	a2i 14	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑦 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)))
127	126	a1i 11	. . . 4 ⊢ (𝑦 ∈ Fin → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑦 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp))))
128	10, 16, 22, 28, 33, 127	findcard2 8765	. . 3 ⊢ (𝐴 ∈ Fin → ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝐴 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp)))
129	2, 128	mpcom 38	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝐴 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp))
130	1, 129	mpi 20	1 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1088 = wceq 1542 ∈ wcel 2114 ∀wral 3053 Vcvv 3398 ⦋csb 3790 ∪ cun 3841 ∩ cin 3842 ⊆ wss 3843 ∅c0 4211 {csn 4516 ∪ cuni 4796 ∪ ciun 4881 (class class class)co 7172 Fincfn 8557 ↾_t crest 16799 Topctop 21646 Compccmp 22139

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2710 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5232 ax-pr 5296 ax-un 7481

This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-ral 3058 df-rex 3059 df-reu 3060 df-rab 3062 df-v 3400 df-sbc 3681 df-csb 3791 df-dif 3846 df-un 3848 df-in 3850 df-ss 3860 df-pss 3862 df-nul 4212 df-if 4415 df-pw 4490 df-sn 4517 df-pr 4519 df-tp 4521 df-op 4523 df-uni 4797 df-int 4837 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5429 df-eprel 5434 df-po 5442 df-so 5443 df-fr 5483 df-we 5485 df-xp 5531 df-rel 5532 df-cnv 5533 df-co 5534 df-dm 5535 df-rn 5536 df-res 5537 df-ima 5538 df-ord 6175 df-on 6176 df-lim 6177 df-suc 6178 df-iota 6297 df-fun 6341 df-fn 6342 df-f 6343 df-f1 6344 df-fo 6345 df-f1o 6346 df-fv 6347 df-ov 7175 df-oprab 7176 df-mpo 7177 df-om 7602 df-1st 7716 df-2nd 7717 df-1o 8133 df-er 8322 df-en 8558 df-dom 8559 df-fin 8561 df-fi 8950 df-rest 16801 df-topgen 16822 df-top 21647 df-topon 21664 df-bases 21699 df-cmp 22140

This theorem is referenced by: xkococnlem 22412

W3C validator