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 21017

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 3587	. 2 ⊢ 𝐴 ⊆ 𝐴
2		simp2 1055	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → 𝐴 ∈ Fin)
3		sseq1 3589	. . . . . 6 ⊢ (𝑡 = ∅ → (𝑡 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴))
4		iuneq1 4470	. . . . . . . . 9 ⊢ (𝑡 = ∅ → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ ∅ 𝐵)
5		0iun 4513	. . . . . . . . 9 ⊢ ∪ 𝑥 ∈ ∅ 𝐵 = ∅
6	4, 5	syl6eq 2660	. . . . . . . 8 ⊢ (𝑡 = ∅ → ∪ 𝑥 ∈ 𝑡 𝐵 = ∅)
7	6	oveq2d 6565	. . . . . . 7 ⊢ (𝑡 = ∅ → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾_t ∅))
8	7	eleq1d 2672	. . . . . 6 ⊢ (𝑡 = ∅ → ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾_t ∅) ∈ Comp))
9	3, 8	imbi12d 333	. . . . 5 ⊢ (𝑡 = ∅ → ((𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ (∅ ⊆ 𝐴 → (𝐽 ↾_t ∅) ∈ Comp)))
10	9	imbi2d 329	. . . 4 ⊢ (𝑡 = ∅ → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (∅ ⊆ 𝐴 → (𝐽 ↾_t ∅) ∈ Comp))))
11		sseq1 3589	. . . . . 6 ⊢ (𝑡 = 𝑦 → (𝑡 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴))
12		iuneq1 4470	. . . . . . . 8 ⊢ (𝑡 = 𝑦 → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ 𝑦 𝐵)
13	12	oveq2d 6565	. . . . . . 7 ⊢ (𝑡 = 𝑦 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵))
14	13	eleq1d 2672	. . . . . 6 ⊢ (𝑡 = 𝑦 → ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp))
15	11, 14	imbi12d 333	. . . . 5 ⊢ (𝑡 = 𝑦 → ((𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ (𝑦 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)))
16	15	imbi2d 329	. . . 4 ⊢ (𝑡 = 𝑦 → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑦 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp))))
17		sseq1 3589	. . . . . 6 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → (𝑡 ⊆ 𝐴 ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐴))
18		iuneq1 4470	. . . . . . . 8 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
19	18	oveq2d 6565	. . . . . . 7 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵))
20	19	eleq1d 2672	. . . . . 6 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp))
21	17, 20	imbi12d 333	. . . . 5 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → ((𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)))
22	21	imbi2d 329	. . . 4 ⊢ (𝑡 = (𝑦 ∪ {𝑧}) → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp))))
23		sseq1 3589	. . . . . 6 ⊢ (𝑡 = 𝐴 → (𝑡 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴))
24		iuneq1 4470	. . . . . . . 8 ⊢ (𝑡 = 𝐴 → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵)
25	24	oveq2d 6565	. . . . . . 7 ⊢ (𝑡 = 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) = (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵))
26	25	eleq1d 2672	. . . . . 6 ⊢ (𝑡 = 𝐴 → ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp ↔ (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp))
27	23, 26	imbi12d 333	. . . . 5 ⊢ (𝑡 = 𝐴 → ((𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp) ↔ (𝐴 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp)))
28	27	imbi2d 329	. . . 4 ⊢ (𝑡 = 𝐴 → (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝑡 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑡 𝐵) ∈ Comp)) ↔ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝐴 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp))))
29		rest0 20783	. . . . . . 7 ⊢ (𝐽 ∈ Top → (𝐽 ↾_t ∅) = {∅})
30		0cmp 21007	. . . . . . 7 ⊢ {∅} ∈ Comp
31	29, 30	syl6eqel 2696	. . . . . 6 ⊢ (𝐽 ∈ Top → (𝐽 ↾_t ∅) ∈ Comp)
32	31	3ad2ant1 1075	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝐽 ↾_t ∅) ∈ Comp)
33	32	a1d 25	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (∅ ⊆ 𝐴 → (𝐽 ↾_t ∅) ∈ Comp))
34		ssun1 3738	. . . . . . . . 9 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧})
35		id 22	. . . . . . . . 9 ⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
36	34, 35	syl5ss 3579	. . . . . . . 8 ⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → 𝑦 ⊆ 𝐴)
37	36	imim1i 61	. . . . . . 7 ⊢ ((𝑦 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp))
38		simpl1 1057	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → 𝐽 ∈ Top)
39		iunxun 4541	. . . . . . . . . . . 12 ⊢ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 = (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵)
40		simprr 792	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)
41		cmptop 21008	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Top)
42		restrcl 20771	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Top → (𝐽 ∈ V ∧ ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V))
43	42	simprd 478	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Top → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V)
44	40, 41, 43	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V)
45		nfcv 2751	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡𝐵
46		nfcsb1v 3515	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥⦋𝑡 / 𝑥⦌𝐵
47		csbeq1a 3508	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑡 → 𝐵 = ⦋𝑡 / 𝑥⦌𝐵)
48	45, 46, 47	cbviun 4493	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑥 ∈ {𝑧}𝐵 = ∪ 𝑡 ∈ {𝑧}⦋𝑡 / 𝑥⦌𝐵
49		vex 3176	. . . . . . . . . . . . . . . 16 ⊢ 𝑧 ∈ V
50		csbeq1 3502	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑧 → ⦋𝑡 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵)
51	49, 50	iunxsn 4539	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑡 ∈ {𝑧}⦋𝑡 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵
52	48, 51	eqtri 2632	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑥 ∈ {𝑧}𝐵 = ⦋𝑧 / 𝑥⦌𝐵
53		ssun2 3739	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑧} ⊆ (𝑦 ∪ {𝑧})
54		simprl 790	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
55	53, 54	syl5ss 3579	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → {𝑧} ⊆ 𝐴)
56	49	snss 4259	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝐴 ↔ {𝑧} ⊆ 𝐴)
57	55, 56	sylibr 223	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → 𝑧 ∈ 𝐴)
58		simpl3 1059	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp)
59		nfv 1830	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡(𝐽 ↾_t 𝐵) ∈ Comp
60		nfcv 2751	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥𝐽
61		nfcv 2751	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥 ↾_t
62	60, 61, 46	nfov 6575	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵)
63	62	nfel1 2765	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥(𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp
64	47	oveq2d 6565	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑡 → (𝐽 ↾_t 𝐵) = (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵))
65	64	eleq1d 2672	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑡 → ((𝐽 ↾_t 𝐵) ∈ Comp ↔ (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp))
66	59, 63, 65	cbvral 3143	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp ↔ ∀𝑡 ∈ 𝐴 (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp)
67	58, 66	sylib 207	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∀𝑡 ∈ 𝐴 (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp)
68	50	oveq2d 6565	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑧 → (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) = (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵))
69	68	eleq1d 2672	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑧 → ((𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp ↔ (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Comp))
70	69	rspcv 3278	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝐴 → (∀𝑡 ∈ 𝐴 (𝐽 ↾_t ⦋𝑡 / 𝑥⦌𝐵) ∈ Comp → (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Comp))
71	57, 67, 70	sylc 63	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Comp)
72		cmptop 21008	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Comp → (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Top)
73		restrcl 20771	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Top → (𝐽 ∈ V ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ V))
74	73	simprd 478	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) ∈ Top → ⦋𝑧 / 𝑥⦌𝐵 ∈ V)
75	71, 72, 74	3syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ⦋𝑧 / 𝑥⦌𝐵 ∈ V)
76	52, 75	syl5eqel 2692	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ 𝑥 ∈ {𝑧}𝐵 ∈ V)
77		unexg 6857	. . . . . . . . . . . . 13 ⊢ ((∪ 𝑥 ∈ 𝑦 𝐵 ∈ V ∧ ∪ 𝑥 ∈ {𝑧}𝐵 ∈ V) → (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵) ∈ V)
78	44, 76, 77	syl2anc 691	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵) ∈ V)
79	39, 78	syl5eqel 2692	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V)
80		resttop 20774	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Top)
81	38, 79, 80	syl2anc 691	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Top)
82		eqid 2610	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝐽 = ∪ 𝐽
83	82	restin 20780	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
84	38, 79, 83	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
85	84	unieqd 4382	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ∪ (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
86		inss2 3796	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝐽
87		fiuncmp.1	. . . . . . . . . . . . . 14 ⊢ 𝑋 = ∪ 𝐽
88	86, 87	sseqtr4i 3601	. . . . . . . . . . . . 13 ⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) ⊆ 𝑋
89	87	restuni 20776	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) ⊆ 𝑋) → (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ∪ (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
90	38, 88, 89	sylancl 693	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ∪ (𝐽 ↾_t (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽)))
91	85, 90	eqtr4d 2647	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽))
92	52	uneq2i 3726	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵) = (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵)
93	39, 92	eqtri 2632	. . . . . . . . . . . . 13 ⊢ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 = (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵)
94	93	ineq1i 3772	. . . . . . . . . . . 12 ⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵) ∩ ∪ 𝐽)
95		indir 3834	. . . . . . . . . . . 12 ⊢ ((∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋𝑧 / 𝑥⦌𝐵) ∩ ∪ 𝐽) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))
96	94, 95	eqtri 2632	. . . . . . . . . . 11 ⊢ (∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∩ ∪ 𝐽) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))
97	91, 96	syl6eq 2660	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
98		inss1 3795	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ 𝑦 𝐵
99		ssun1 3738	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵)
100	99, 39	sseqtr4i 3601	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
101	98, 100	sstri 3577	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
102	101	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
103		restabs 20779	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)))
104	38, 102, 79, 103	syl3anc 1318	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)))
105	82	restin 20780	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V) → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) = (𝐽 ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)))
106	38, 44, 105	syl2anc 691	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) = (𝐽 ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)))
107	104, 106	eqtr4d 2647	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵))
108	107, 40	eqeltrd 2688	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) ∈ Comp)
109		inss1 3795	. . . . . . . . . . . . . . 15 ⊢ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ⦋𝑧 / 𝑥⦌𝐵
110		ssun2 3739	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑥 ∈ {𝑧}𝐵 ⊆ (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵)
111	110, 39	sseqtr4i 3601	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑥 ∈ {𝑧}𝐵 ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
112	52, 111	eqsstr3i 3599	. . . . . . . . . . . . . . 15 ⊢ ⦋𝑧 / 𝑥⦌𝐵 ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
113	109, 112	sstri 3577	. . . . . . . . . . . . . 14 ⊢ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵
114	113	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
115		restabs 20779	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽) ⊆ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∧ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ V) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
116	38, 114, 79, 115	syl3anc 1318	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
117	82	restin 20780	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ V) → (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) = (𝐽 ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
118	38, 75, 117	syl2anc 691	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵) = (𝐽 ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)))
119	116, 118	eqtr4d 2647	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) = (𝐽 ↾_t ⦋𝑧 / 𝑥⦌𝐵))
120	119, 71	eqeltrd 2688	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) ∈ Comp)
121		eqid 2610	. . . . . . . . . . 11 ⊢ ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
122	121	uncmp 21016	. . . . . . . . . 10 ⊢ ((((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Top ∧ ∪ (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) = ((∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽) ∪ (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽))) ∧ (((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽)) ∈ Comp ∧ ((𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ↾_t (⦋𝑧 / 𝑥⦌𝐵 ∩ ∪ 𝐽)) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)
123	81, 97, 108, 120, 122	syl22anc 1319	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝐽 ↾_t ∪ 𝑥 ∈ 𝑦 𝐵) ∈ Comp)) → (𝐽 ↾_t ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵) ∈ Comp)
124	123	exp32 629	. . . . . . . 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 33	. . . . . 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 8085	. . 3 ⊢ (𝐴 ∈ Fin → ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾_t 𝐵) ∈ Comp) → (𝐴 ⊆ 𝐴 → (𝐽 ↾_t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp)))
130	2, 129	mpcom 37	. 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 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ∀wral 2896 Vcvv 3173 ⦋csb 3499 ∪ cun 3538 ∩ cin 3539 ⊆ wss 3540 ∅c0 3874 {csn 4125 ∪ cuni 4372 ∪ ciun 4455 (class class class)co 6549 Fincfn 7841 ↾_t crest 15904 Topctop 20517 Compccmp 20999

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-reu 2903 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-en 7842 df-dom 7843 df-fin 7845 df-fi 8200 df-rest 15906 df-topgen 15927 df-top 20521 df-bases 20522 df-topon 20523 df-cmp 21000

This theorem is referenced by: xkococnlem 21272

W3C validator