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 23412

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 4006	. 2 ⊢ 𝐴 ⊆ 𝐴
2		simp2 1138	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → 𝐴 ∈ Fin)
3		sseq1 4009	. . . . . 6 ⊢ (𝑡 = ∅ → (𝑡 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴))
4		iuneq1 5008	. . . . . . . . 9 ⊢ (𝑡 = ∅ → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ ∅ 𝐵)
5		0iun 5063	. . . . . . . . 9 ⊢ ∪ 𝑥 ∈ ∅ 𝐵 = ∅
6	4, 5	eqtrdi 2793	. . . . . . . 8 ⊢ (𝑡 = ∅ → ∪ 𝑥 ∈ 𝑡 𝐵 = ∅)
7	6	oveq2d 7447	. . . . . . 7 ⊢ (𝑡 = ∅ → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾_t ∅))
8	7	eleq1d 2826	. . . . . 6 ⊢ (𝑡 = ∅ → ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾_t ∅) ∈ Comp))
9	3, 8	imbi12d 344	. . . . 5 ⊢ (𝑡 = ∅ → ((𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ (∅ ⊆ 𝐴 → (𝐽 ↾_t ∅) ∈ Comp)))
10	9	imbi2d 340	. . . 4 ⊢ (𝑡 = ∅ → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (∅ ⊆ 𝐴 → (𝐽 ↾_t ∅) ∈ Comp))))
11		sseq1 4009	. . . . . 6 ⊢ (𝑡 = 𝑦 → (𝑡 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴))
12		iuneq1 5008	. . . . . . . 8 ⊢ (𝑡 = 𝑦 → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ 𝑦 𝐵)
13	12	oveq2d 7447	. . . . . . 7 ⊢ (𝑡 = 𝑦 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵))
14	13	eleq1d 2826	. . . . . 6 ⊢ (𝑡 = 𝑦 → ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp))
15	11, 14	imbi12d 344	. . . . 5 ⊢ (𝑡 = 𝑦 → ((𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ (𝑦 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)))
16	15	imbi2d 340	. . . 4 ⊢ (𝑡 = 𝑦 → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑦 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp))))
17		sseq1 4009	. . . . . 6 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → (𝑡 ⊆ 𝐴 ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐴))
18		iuneq1 5008	. . . . . . . 8 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
19	18	oveq2d 7447	. . . . . . 7 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵))
20	19	eleq1d 2826	. . . . . 6 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp))
21	17, 20	imbi12d 344	. . . . 5 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → ((𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)))
22	21	imbi2d 340	. . . 4 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp))))
23		sseq1 4009	. . . . . 6 ⊢ (𝑡 = 𝐴 → (𝑡 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴))
24		iuneq1 5008	. . . . . . . 8 ⊢ (𝑡 = 𝐴 → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵)
25	24	oveq2d 7447	. . . . . . 7 ⊢ (𝑡 = 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵))
26	25	eleq1d 2826	. . . . . 6 ⊢ (𝑡 = 𝐴 → ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp))
27	23, 26	imbi12d 344	. . . . 5 ⊢ (𝑡 = 𝐴 → ((𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ (𝐴 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp)))
28	27	imbi2d 340	. . . 4 ⊢ (𝑡 = 𝐴 → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝐴 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp))))
29		rest0 23177	. . . . . . 7 ⊢ (𝐽 ∈ Top → (𝐽 ↾_t ∅) = {∅})
30		0cmp 23402	. . . . . . 7 ⊢ {∅} ∈ Comp
31	29, 30	eqeltrdi 2849	. . . . . 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 4178	. . . . . . . . 9 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧})
35		id 22	. . . . . . . . 9 ⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
36	34, 35	sstrid 3995	. . . . . . . 8 ⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → 𝑦 ⊆ 𝐴)
37	36	imim1i 63	. . . . . . 7 ⊢ ((𝑦 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp))
38		simpl1 1192	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → 𝐽 ∈ Top)
39		iunxun 5094	. . . . . . . . . . . 12 ⊢ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 = (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵)
40		simprr 773	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)
41		cmptop 23403	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Top)
42		restrcl 23165	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Top → (𝐽 ∈ V ∧ ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V))
43	42	simprd 495	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Top → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V)
44	40, 41, 43	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V)
45		nfcv 2905	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡𝐵
46		nfcsb1v 3923	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥⦋𝑡 / 𝑥⦌𝐵
47		csbeq1a 3913	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑡 → 𝐵 = ⦋𝑡 / 𝑥⦌𝐵)
48	45, 46, 47	cbviun 5036	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑥 ∈ {𝑧}𝐵 = ∪ 𝑡 ∈ {𝑧}⦋𝑡 / 𝑥⦌𝐵
49		vex 3484	. . . . . . . . . . . . . . . 16 ⊢ 𝑧 ∈ V
50		csbeq1 3902	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑧 → ⦋𝑡 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵)
51	49, 50	iunxsn 5091	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑡 ∈ {𝑧}⦋𝑡 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵
52	48, 51	eqtri 2765	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑥 ∈ {𝑧}𝐵 = ⦋𝑧 / 𝑥⦌𝐵
53	50	oveq2d 7447	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑧 → (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) = (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵))
54	53	eleq1d 2826	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑧 → ((𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp ↔ (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Comp))
55		simpl3 1194	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp)
56		nfv 1914	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡(𝐽 ↾_t 𝐵) ∈ Comp
57		nfcv 2905	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥𝐽
58		nfcv 2905	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥 ↾_t
59	57, 58, 46	nfov 7461	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵)
60	59	nfel1 2922	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥(𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp
61	47	oveq2d 7447	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑡 → (𝐽 ↾_t 𝐵) = (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵))
62	61	eleq1d 2826	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑡 → ((𝐽 ↾_t 𝐵) ∈ Comp ↔ (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp))
63	56, 60, 62	cbvralw 3306	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp ↔ ∀𝑡 ∈ 𝐴 (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp)
64	55, 63	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∀𝑡 ∈ 𝐴 (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp)
65		ssun2 4179	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑧} ⊆ (𝑦 ∪ {𝑧})
66		simprl 771	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
67	65, 66	sstrid 3995	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → {𝑧} ⊆ 𝐴)
68	49	snss 4785	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝐴 ↔ {𝑧} ⊆ 𝐴)
69	67, 68	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → 𝑧 ∈ 𝐴)
70	54, 64, 69	rspcdva 3623	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Comp)
71		cmptop 23403	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Comp → (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Top)
72		restrcl 23165	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Top → (𝐽 ∈ V ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ V))
73	72	simprd 495	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Top → ⦋𝑧 / 𝑥⦌𝐵 ∈ V)
74	70, 71, 73	3syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ⦋𝑧 / 𝑥⦌𝐵 ∈ V)
75	52, 74	eqeltrid 2845	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ 𝑥 ∈ {𝑧}𝐵 ∈ V)
76		unexg 7763	. . . . . . . . . . . . 13 ⊢ ((∪ 𝑥 ∈ 𝑦 𝐵 ∈ V ∧ ∪ 𝑥 ∈ {𝑧}𝐵 ∈ V) → (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵) ∈ V)
77	44, 75, 76	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵) ∈ V)
78	39, 77	eqeltrid 2845	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V)
79		resttop 23168	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Top)
80	38, 78, 79	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Top)
81		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝐽 = ∪ 𝐽
82	81	restin 23174	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
83	38, 78, 82	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
84	83	unieqd 4920	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ∪ (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
85		inss2 4238	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝐽
86		fiuncmp.1	. . . . . . . . . . . . . 14 ⊢ 𝑋 = ∪ 𝐽
87	85, 86	sseqtrri 4033	. . . . . . . . . . . . 13 ⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) ⊆ 𝑋
88	86	restuni 23170	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) ⊆ 𝑋) → (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ∪ (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
89	38, 87, 88	sylancl 586	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ∪ (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
90	84, 89	eqtr4d 2780	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽))
91	52	uneq2i 4165	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵) = (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵)
92	39, 91	eqtri 2765	. . . . . . . . . . . . 13 ⊢ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 = (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵)
93	92	ineq1i 4216	. . . . . . . . . . . 12 ⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵) ∩ ∪ 𝐽)
94		indir 4286	. . . . . . . . . . . 12 ⊢ ((∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵) ∩ ∪ 𝐽) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))
95	93, 94	eqtri 2765	. . . . . . . . . . 11 ⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))
96	90, 95	eqtrdi 2793	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
97		inss1 4237	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ 𝑦 𝐵
98		ssun1 4178	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵)
99	98, 39	sseqtrri 4033	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
100	97, 99	sstri 3993	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
101	100	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
102		restabs 23173	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)))
103	38, 101, 78, 102	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)))
104	81	restin 23174	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V) → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) = (𝐽 ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)))
105	38, 44, 104	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) = (𝐽 ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)))
106	103, 105	eqtr4d 2780	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵))
107	106, 40	eqeltrd 2841	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) ∈ Comp)
108		inss1 4237	. . . . . . . . . . . . . . 15 ⊢ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ⦋𝑧 / 𝑥⦌𝐵
109		ssun2 4179	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑥 ∈ {𝑧}𝐵 ⊆ (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵)
110	109, 39	sseqtrri 4033	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑥 ∈ {𝑧}𝐵 ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
111	52, 110	eqsstrri 4031	. . . . . . . . . . . . . . 15 ⊢ ⦋𝑧 / 𝑥⦌𝐵 ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
112	108, 111	sstri 3993	. . . . . . . . . . . . . 14 ⊢ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
113	112	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
114		restabs 23173	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
115	38, 113, 78, 114	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
116	81	restin 23174	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ V) → (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) = (𝐽 ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
117	38, 74, 116	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) = (𝐽 ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
118	115, 117	eqtr4d 2780	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵))
119	118, 70	eqeltrd 2841	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) ∈ Comp)
120		eqid 2737	. . . . . . . . . . 11 ⊢ ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
121	120	uncmp 23411	. . . . . . . . . 10 ⊢ ((((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Top ∧ ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))) ∧ (((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) ∈ Comp ∧ ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)
122	80, 96, 107, 119, 121	syl22anc 839	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)
123	122	exp32 420	. . . . . . . 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 9204	. . 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 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ∀wral 3061 Vcvv 3480 ⦋csb 3899 ∪ cun 3949 ∩ cin 3950 ⊆ wss 3951 ∅c0 4333 {csn 4626 ∪ cuni 4907 ∪ ciun 4991 (class class class)co 7431 Fincfn 8985 ↾_t crest 17465 Topctop 22899 Compccmp 23394

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8014 df-2nd 8015 df-1o 8506 df-en 8986 df-dom 8987 df-fin 8989 df-fi 9451 df-rest 17467 df-topgen 17488 df-top 22900 df-topon 22917 df-bases 22953 df-cmp 23395

This theorem is referenced by: xkococnlem 23667

W3C validator