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 23128

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 4003	. 2 ⊢ 𝐴 ⊆ 𝐴
2		simp2 1135	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → 𝐴 ∈ Fin)
3		sseq1 4006	. . . . . 6 ⊢ (𝑡 = ∅ → (𝑡 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴))
4		iuneq1 5012	. . . . . . . . 9 ⊢ (𝑡 = ∅ → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ ∅ 𝐵)
5		0iun 5065	. . . . . . . . 9 ⊢ ∪ 𝑥 ∈ ∅ 𝐵 = ∅
6	4, 5	eqtrdi 2786	. . . . . . . 8 ⊢ (𝑡 = ∅ → ∪ 𝑥 ∈ 𝑡 𝐵 = ∅)
7	6	oveq2d 7427	. . . . . . 7 ⊢ (𝑡 = ∅ → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾_t ∅))
8	7	eleq1d 2816	. . . . . 6 ⊢ (𝑡 = ∅ → ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾_t ∅) ∈ Comp))
9	3, 8	imbi12d 343	. . . . 5 ⊢ (𝑡 = ∅ → ((𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ (∅ ⊆ 𝐴 → (𝐽 ↾_t ∅) ∈ Comp)))
10	9	imbi2d 339	. . . 4 ⊢ (𝑡 = ∅ → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (∅ ⊆ 𝐴 → (𝐽 ↾_t ∅) ∈ Comp))))
11		sseq1 4006	. . . . . 6 ⊢ (𝑡 = 𝑦 → (𝑡 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴))
12		iuneq1 5012	. . . . . . . 8 ⊢ (𝑡 = 𝑦 → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ 𝑦 𝐵)
13	12	oveq2d 7427	. . . . . . 7 ⊢ (𝑡 = 𝑦 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵))
14	13	eleq1d 2816	. . . . . 6 ⊢ (𝑡 = 𝑦 → ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp))
15	11, 14	imbi12d 343	. . . . 5 ⊢ (𝑡 = 𝑦 → ((𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ (𝑦 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)))
16	15	imbi2d 339	. . . 4 ⊢ (𝑡 = 𝑦 → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑦 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp))))
17		sseq1 4006	. . . . . 6 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → (𝑡 ⊆ 𝐴 ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐴))
18		iuneq1 5012	. . . . . . . 8 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
19	18	oveq2d 7427	. . . . . . 7 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵))
20	19	eleq1d 2816	. . . . . 6 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp))
21	17, 20	imbi12d 343	. . . . 5 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → ((𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)))
22	21	imbi2d 339	. . . 4 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp))))
23		sseq1 4006	. . . . . 6 ⊢ (𝑡 = 𝐴 → (𝑡 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴))
24		iuneq1 5012	. . . . . . . 8 ⊢ (𝑡 = 𝐴 → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵)
25	24	oveq2d 7427	. . . . . . 7 ⊢ (𝑡 = 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵))
26	25	eleq1d 2816	. . . . . 6 ⊢ (𝑡 = 𝐴 → ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp))
27	23, 26	imbi12d 343	. . . . 5 ⊢ (𝑡 = 𝐴 → ((𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ (𝐴 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp)))
28	27	imbi2d 339	. . . 4 ⊢ (𝑡 = 𝐴 → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝐴 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp))))
29		rest0 22893	. . . . . . 7 ⊢ (𝐽 ∈ Top → (𝐽 ↾_t ∅) = {∅})
30		0cmp 23118	. . . . . . 7 ⊢ {∅} ∈ Comp
31	29, 30	eqeltrdi 2839	. . . . . 6 ⊢ (𝐽 ∈ Top → (𝐽 ↾_t ∅) ∈ Comp)
32	31	3ad2ant1 1131	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝐽 ↾_t ∅) ∈ Comp)
33	32	a1d 25	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (∅ ⊆ 𝐴 → (𝐽 ↾_t ∅) ∈ Comp))
34		ssun1 4171	. . . . . . . . 9 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧})
35		id 22	. . . . . . . . 9 ⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
36	34, 35	sstrid 3992	. . . . . . . 8 ⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → 𝑦 ⊆ 𝐴)
37	36	imim1i 63	. . . . . . 7 ⊢ ((𝑦 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp))
38		simpl1 1189	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → 𝐽 ∈ Top)
39		iunxun 5096	. . . . . . . . . . . 12 ⊢ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 = (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵)
40		simprr 769	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)
41		cmptop 23119	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Top)
42		restrcl 22881	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Top → (𝐽 ∈ V ∧ ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V))
43	42	simprd 494	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Top → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V)
44	40, 41, 43	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V)
45		nfcv 2901	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡𝐵
46		nfcsb1v 3917	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥⦋𝑡 / 𝑥⦌𝐵
47		csbeq1a 3906	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑡 → 𝐵 = ⦋𝑡 / 𝑥⦌𝐵)
48	45, 46, 47	cbviun 5038	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑥 ∈ {𝑧}𝐵 = ∪ 𝑡 ∈ {𝑧}⦋𝑡 / 𝑥⦌𝐵
49		vex 3476	. . . . . . . . . . . . . . . 16 ⊢ 𝑧 ∈ V
50		csbeq1 3895	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑧 → ⦋𝑡 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵)
51	49, 50	iunxsn 5093	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑡 ∈ {𝑧}⦋𝑡 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵
52	48, 51	eqtri 2758	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑥 ∈ {𝑧}𝐵 = ⦋𝑧 / 𝑥⦌𝐵
53	50	oveq2d 7427	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑧 → (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) = (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵))
54	53	eleq1d 2816	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑧 → ((𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp ↔ (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Comp))
55		simpl3 1191	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp)
56		nfv 1915	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡(𝐽 ↾_t 𝐵) ∈ Comp
57		nfcv 2901	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥𝐽
58		nfcv 2901	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥 ↾_t
59	57, 58, 46	nfov 7441	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵)
60	59	nfel1 2917	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥(𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp
61	47	oveq2d 7427	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑡 → (𝐽 ↾_t 𝐵) = (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵))
62	61	eleq1d 2816	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑡 → ((𝐽 ↾_t 𝐵) ∈ Comp ↔ (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp))
63	56, 60, 62	cbvralw 3301	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp ↔ ∀𝑡 ∈ 𝐴 (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp)
64	55, 63	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∀𝑡 ∈ 𝐴 (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp)
65		ssun2 4172	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑧} ⊆ (𝑦 ∪ {𝑧})
66		simprl 767	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
67	65, 66	sstrid 3992	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → {𝑧} ⊆ 𝐴)
68	49	snss 4788	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝐴 ↔ {𝑧} ⊆ 𝐴)
69	67, 68	sylibr 233	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → 𝑧 ∈ 𝐴)
70	54, 64, 69	rspcdva 3612	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Comp)
71		cmptop 23119	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Comp → (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Top)
72		restrcl 22881	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Top → (𝐽 ∈ V ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ V))
73	72	simprd 494	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Top → ⦋𝑧 / 𝑥⦌𝐵 ∈ V)
74	70, 71, 73	3syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ⦋𝑧 / 𝑥⦌𝐵 ∈ V)
75	52, 74	eqeltrid 2835	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ 𝑥 ∈ {𝑧}𝐵 ∈ V)
76		unexg 7738	. . . . . . . . . . . . 13 ⊢ ((∪ 𝑥 ∈ 𝑦 𝐵 ∈ V ∧ ∪ 𝑥 ∈ {𝑧}𝐵 ∈ V) → (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵) ∈ V)
77	44, 75, 76	syl2anc 582	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵) ∈ V)
78	39, 77	eqeltrid 2835	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V)
79		resttop 22884	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Top)
80	38, 78, 79	syl2anc 582	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Top)
81		eqid 2730	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝐽 = ∪ 𝐽
82	81	restin 22890	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
83	38, 78, 82	syl2anc 582	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
84	83	unieqd 4921	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ∪ (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
85		inss2 4228	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝐽
86		fiuncmp.1	. . . . . . . . . . . . . 14 ⊢ 𝑋 = ∪ 𝐽
87	85, 86	sseqtrri 4018	. . . . . . . . . . . . 13 ⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) ⊆ 𝑋
88	86	restuni 22886	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) ⊆ 𝑋) → (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ∪ (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
89	38, 87, 88	sylancl 584	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ∪ (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
90	84, 89	eqtr4d 2773	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽))
91	52	uneq2i 4159	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵) = (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵)
92	39, 91	eqtri 2758	. . . . . . . . . . . . 13 ⊢ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 = (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵)
93	92	ineq1i 4207	. . . . . . . . . . . 12 ⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵) ∩ ∪ 𝐽)
94		indir 4274	. . . . . . . . . . . 12 ⊢ ((∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵) ∩ ∪ 𝐽) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))
95	93, 94	eqtri 2758	. . . . . . . . . . 11 ⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))
96	90, 95	eqtrdi 2786	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
97		inss1 4227	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ 𝑦 𝐵
98		ssun1 4171	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵)
99	98, 39	sseqtrri 4018	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
100	97, 99	sstri 3990	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
101	100	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
102		restabs 22889	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)))
103	38, 101, 78, 102	syl3anc 1369	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)))
104	81	restin 22890	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V) → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) = (𝐽 ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)))
105	38, 44, 104	syl2anc 582	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) = (𝐽 ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)))
106	103, 105	eqtr4d 2773	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵))
107	106, 40	eqeltrd 2831	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) ∈ Comp)
108		inss1 4227	. . . . . . . . . . . . . . 15 ⊢ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ⦋𝑧 / 𝑥⦌𝐵
109		ssun2 4172	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑥 ∈ {𝑧}𝐵 ⊆ (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵)
110	109, 39	sseqtrri 4018	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑥 ∈ {𝑧}𝐵 ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
111	52, 110	eqsstrri 4016	. . . . . . . . . . . . . . 15 ⊢ ⦋𝑧 / 𝑥⦌𝐵 ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
112	108, 111	sstri 3990	. . . . . . . . . . . . . 14 ⊢ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
113	112	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
114		restabs 22889	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
115	38, 113, 78, 114	syl3anc 1369	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
116	81	restin 22890	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ V) → (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) = (𝐽 ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
117	38, 74, 116	syl2anc 582	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) = (𝐽 ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
118	115, 117	eqtr4d 2773	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵))
119	118, 70	eqeltrd 2831	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) ∈ Comp)
120		eqid 2730	. . . . . . . . . . 11 ⊢ ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
121	120	uncmp 23127	. . . . . . . . . 10 ⊢ ((((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Top ∧ ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))) ∧ (((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) ∈ Comp ∧ ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)
122	80, 96, 107, 119, 121	syl22anc 835	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)
123	122	exp32 419	. . . . . . . 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 9166	. . 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 394 ∧ w3a 1085 = wceq 1539 ∈ wcel 2104 ∀wral 3059 Vcvv 3472 ⦋csb 3892 ∪ cun 3945 ∩ cin 3946 ⊆ wss 3947 ∅c0 4321 {csn 4627 ∪ cuni 4907 ∪ ciun 4996 (class class class)co 7411 Fincfn 8941 ↾_t crest 17370 Topctop 22615 Compccmp 23110

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 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-ral 3060 df-rex 3069 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7858 df-1st 7977 df-2nd 7978 df-1o 8468 df-er 8705 df-en 8942 df-dom 8943 df-fin 8945 df-fi 9408 df-rest 17372 df-topgen 17393 df-top 22616 df-topon 22633 df-bases 22669 df-cmp 23111

This theorem is referenced by: xkococnlem 23383

W3C validator