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 21207

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 3624	. 2 ⊢ 𝐴 ⊆ 𝐴
2		simp2 1062	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → 𝐴 ∈ Fin)
3		sseq1 3626	. . . . . 6 ⊢ (𝑡 = ∅ → (𝑡 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴))
4		iuneq1 4534	. . . . . . . . 9 ⊢ (𝑡 = ∅ → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ ∅ 𝐵)
5		0iun 4577	. . . . . . . . 9 ⊢ ∪ 𝑥 ∈ ∅ 𝐵 = ∅
6	4, 5	syl6eq 2672	. . . . . . . 8 ⊢ (𝑡 = ∅ → ∪ 𝑥 ∈ 𝑡 𝐵 = ∅)
7	6	oveq2d 6666	. . . . . . 7 ⊢ (𝑡 = ∅ → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾_t ∅))
8	7	eleq1d 2686	. . . . . 6 ⊢ (𝑡 = ∅ → ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾_t ∅) ∈ Comp))
9	3, 8	imbi12d 334	. . . . 5 ⊢ (𝑡 = ∅ → ((𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ (∅ ⊆ 𝐴 → (𝐽 ↾_t ∅) ∈ Comp)))
10	9	imbi2d 330	. . . 4 ⊢ (𝑡 = ∅ → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (∅ ⊆ 𝐴 → (𝐽 ↾_t ∅) ∈ Comp))))
11		sseq1 3626	. . . . . 6 ⊢ (𝑡 = 𝑦 → (𝑡 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴))
12		iuneq1 4534	. . . . . . . 8 ⊢ (𝑡 = 𝑦 → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ 𝑦 𝐵)
13	12	oveq2d 6666	. . . . . . 7 ⊢ (𝑡 = 𝑦 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵))
14	13	eleq1d 2686	. . . . . 6 ⊢ (𝑡 = 𝑦 → ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp))
15	11, 14	imbi12d 334	. . . . 5 ⊢ (𝑡 = 𝑦 → ((𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ (𝑦 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)))
16	15	imbi2d 330	. . . 4 ⊢ (𝑡 = 𝑦 → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑦 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp))))
17		sseq1 3626	. . . . . 6 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → (𝑡 ⊆ 𝐴 ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐴))
18		iuneq1 4534	. . . . . . . 8 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
19	18	oveq2d 6666	. . . . . . 7 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵))
20	19	eleq1d 2686	. . . . . 6 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp))
21	17, 20	imbi12d 334	. . . . 5 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → ((𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)))
22	21	imbi2d 330	. . . 4 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp))))
23		sseq1 3626	. . . . . 6 ⊢ (𝑡 = 𝐴 → (𝑡 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴))
24		iuneq1 4534	. . . . . . . 8 ⊢ (𝑡 = 𝐴 → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵)
25	24	oveq2d 6666	. . . . . . 7 ⊢ (𝑡 = 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵))
26	25	eleq1d 2686	. . . . . 6 ⊢ (𝑡 = 𝐴 → ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp))
27	23, 26	imbi12d 334	. . . . 5 ⊢ (𝑡 = 𝐴 → ((𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ (𝐴 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp)))
28	27	imbi2d 330	. . . 4 ⊢ (𝑡 = 𝐴 → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝐴 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp))))
29		rest0 20973	. . . . . . 7 ⊢ (𝐽 ∈ Top → (𝐽 ↾_t ∅) = {∅})
30		0cmp 21197	. . . . . . 7 ⊢ {∅} ∈ Comp
31	29, 30	syl6eqel 2709	. . . . . 6 ⊢ (𝐽 ∈ Top → (𝐽 ↾_t ∅) ∈ Comp)
32	31	3ad2ant1 1082	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝐽 ↾_t ∅) ∈ Comp)
33	32	a1d 25	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (∅ ⊆ 𝐴 → (𝐽 ↾_t ∅) ∈ Comp))
34		ssun1 3776	. . . . . . . . 9 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧})
35		id 22	. . . . . . . . 9 ⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
36	34, 35	syl5ss 3614	. . . . . . . 8 ⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → 𝑦 ⊆ 𝐴)
37	36	imim1i 63	. . . . . . 7 ⊢ ((𝑦 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp))
38		simpl1 1064	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → 𝐽 ∈ Top)
39		iunxun 4605	. . . . . . . . . . . 12 ⊢ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 = (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵)
40		simprr 796	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)
41		cmptop 21198	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Top)
42		restrcl 20961	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Top → (𝐽 ∈ V ∧ ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V))
43	42	simprd 479	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Top → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V)
44	40, 41, 43	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V)
45		nfcv 2764	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡𝐵
46		nfcsb1v 3549	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥⦋𝑡 / 𝑥⦌𝐵
47		csbeq1a 3542	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑡 → 𝐵 = ⦋𝑡 / 𝑥⦌𝐵)
48	45, 46, 47	cbviun 4557	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑥 ∈ {𝑧}𝐵 = ∪ 𝑡 ∈ {𝑧}⦋𝑡 / 𝑥⦌𝐵
49		vex 3203	. . . . . . . . . . . . . . . 16 ⊢ 𝑧 ∈ V
50		csbeq1 3536	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑧 → ⦋𝑡 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵)
51	49, 50	iunxsn 4603	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑡 ∈ {𝑧}⦋𝑡 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵
52	48, 51	eqtri 2644	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑥 ∈ {𝑧}𝐵 = ⦋𝑧 / 𝑥⦌𝐵
53		ssun2 3777	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑧} ⊆ (𝑦 ∪ {𝑧})
54		simprl 794	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
55	53, 54	syl5ss 3614	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → {𝑧} ⊆ 𝐴)
56	49	snss 4316	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝐴 ↔ {𝑧} ⊆ 𝐴)
57	55, 56	sylibr 224	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → 𝑧 ∈ 𝐴)
58		simpl3 1066	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp)
59		nfv 1843	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡(𝐽 ↾_t 𝐵) ∈ Comp
60		nfcv 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥𝐽
61		nfcv 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥 ↾_t
62	60, 61, 46	nfov 6676	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵)
63	62	nfel1 2779	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥(𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp
64	47	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑡 → (𝐽 ↾_t 𝐵) = (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵))
65	64	eleq1d 2686	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑡 → ((𝐽 ↾_t 𝐵) ∈ Comp ↔ (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp))
66	59, 63, 65	cbvral 3167	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp ↔ ∀𝑡 ∈ 𝐴 (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp)
67	58, 66	sylib 208	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∀𝑡 ∈ 𝐴 (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp)
68	50	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑧 → (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) = (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵))
69	68	eleq1d 2686	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑧 → ((𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp ↔ (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Comp))
70	69	rspcv 3305	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝐴 → (∀𝑡 ∈ 𝐴 (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp → (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Comp))
71	57, 67, 70	sylc 65	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Comp)
72		cmptop 21198	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Comp → (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Top)
73		restrcl 20961	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Top → (𝐽 ∈ V ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ V))
74	73	simprd 479	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Top → ⦋𝑧 / 𝑥⦌𝐵 ∈ V)
75	71, 72, 74	3syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ⦋𝑧 / 𝑥⦌𝐵 ∈ V)
76	52, 75	syl5eqel 2705	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ 𝑥 ∈ {𝑧}𝐵 ∈ V)
77		unexg 6959	. . . . . . . . . . . . 13 ⊢ ((∪ 𝑥 ∈ 𝑦 𝐵 ∈ V ∧ ∪ 𝑥 ∈ {𝑧}𝐵 ∈ V) → (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵) ∈ V)
78	44, 76, 77	syl2anc 693	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵) ∈ V)
79	39, 78	syl5eqel 2705	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V)
80		resttop 20964	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Top)
81	38, 79, 80	syl2anc 693	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Top)
82		eqid 2622	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝐽 = ∪ 𝐽
83	82	restin 20970	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
84	38, 79, 83	syl2anc 693	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
85	84	unieqd 4446	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ∪ (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
86		inss2 3834	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝐽
87		fiuncmp.1	. . . . . . . . . . . . . 14 ⊢ 𝑋 = ∪ 𝐽
88	86, 87	sseqtr4i 3638	. . . . . . . . . . . . 13 ⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) ⊆ 𝑋
89	87	restuni 20966	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) ⊆ 𝑋) → (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ∪ (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
90	38, 88, 89	sylancl 694	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ∪ (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
91	85, 90	eqtr4d 2659	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽))
92	52	uneq2i 3764	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵) = (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵)
93	39, 92	eqtri 2644	. . . . . . . . . . . . 13 ⊢ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 = (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵)
94	93	ineq1i 3810	. . . . . . . . . . . 12 ⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵) ∩ ∪ 𝐽)
95		indir 3875	. . . . . . . . . . . 12 ⊢ ((∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵) ∩ ∪ 𝐽) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))
96	94, 95	eqtri 2644	. . . . . . . . . . 11 ⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))
97	91, 96	syl6eq 2672	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
98		inss1 3833	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ 𝑦 𝐵
99		ssun1 3776	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵)
100	99, 39	sseqtr4i 3638	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
101	98, 100	sstri 3612	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
102	101	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
103		restabs 20969	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)))
104	38, 102, 79, 103	syl3anc 1326	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)))
105	82	restin 20970	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V) → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) = (𝐽 ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)))
106	38, 44, 105	syl2anc 693	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) = (𝐽 ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)))
107	104, 106	eqtr4d 2659	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵))
108	107, 40	eqeltrd 2701	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) ∈ Comp)
109		inss1 3833	. . . . . . . . . . . . . . 15 ⊢ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ⦋𝑧 / 𝑥⦌𝐵
110		ssun2 3777	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑥 ∈ {𝑧}𝐵 ⊆ (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵)
111	110, 39	sseqtr4i 3638	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑥 ∈ {𝑧}𝐵 ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
112	52, 111	eqsstr3i 3636	. . . . . . . . . . . . . . 15 ⊢ ⦋𝑧 / 𝑥⦌𝐵 ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
113	109, 112	sstri 3612	. . . . . . . . . . . . . 14 ⊢ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
114	113	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
115		restabs 20969	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
116	38, 114, 79, 115	syl3anc 1326	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
117	82	restin 20970	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ V) → (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) = (𝐽 ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
118	38, 75, 117	syl2anc 693	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) = (𝐽 ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
119	116, 118	eqtr4d 2659	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵))
120	119, 71	eqeltrd 2701	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) ∈ Comp)
121		eqid 2622	. . . . . . . . . . 11 ⊢ ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
122	121	uncmp 21206	. . . . . . . . . 10 ⊢ ((((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Top ∧ ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))) ∧ (((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) ∈ Comp ∧ ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)
123	81, 97, 108, 120, 122	syl22anc 1327	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)
124	123	exp32 631	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)))
125	124	a2d 29	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)))
126	37, 125	syl5 34	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → ((𝑦 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)))
127	126	a2i 14	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑦 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)))
128	127	a1i 11	. . . 4 ⊢ (𝑦 ∈ Fin → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑦 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp))))
129	10, 16, 22, 28, 33, 128	findcard2 8200	. . 3 ⊢ (𝐴 ∈ Fin → ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝐴 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp)))
130	2, 129	mpcom 38	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝐴 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp))
131	1, 130	mpi 20	1 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ∀wral 2912 Vcvv 3200 ⦋csb 3533 ∪ cun 3572 ∩ cin 3573 ⊆ wss 3574 ∅c0 3915 {csn 4177 ∪ cuni 4436 ∪ ciun 4520 (class class class)co 6650 Fincfn 7955 ↾_t crest 16081 Topctop 20698 Compccmp 21189

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

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-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-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-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-en 7956 df-dom 7957 df-fin 7959 df-fi 8317 df-rest 16083 df-topgen 16104 df-top 20699 df-topon 20716 df-bases 20750 df-cmp 21190

This theorem is referenced by: xkococnlem 21462

W3C validator