Metamath Proof Explorer

Theorem fiuncmp

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

Ref Expression
Hypothesis fiuncmp.1 ⊢ 𝑋 = ∪ 𝐽
Assertion fiuncmp ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵 ) ∈ Comp )

Proof

Step Hyp Ref Expression
1 fiuncmp.1 ⊢ 𝑋 = ∪ 𝐽
2 ssid ⊢ 𝐴 ⊆ 𝐴
3 simp2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) → 𝐴 ∈ Fin )
4 sseq1 ⊢ ( 𝑡 = ∅ → ( 𝑡 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴 ) )
5 iuneq1 ⊢ ( 𝑡 = ∅ → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ ∅ 𝐵 )
6 0iun ⊢ ∪ 𝑥 ∈ ∅ 𝐵 = ∅
7 5 6 eqtrdi ⊢ ( 𝑡 = ∅ → ∪ 𝑥 ∈ 𝑡 𝐵 = ∅ )
8 7 oveq2d ⊢ ( 𝑡 = ∅ → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵 ) = ( 𝐽 ↾t ∅ ) )
9 8 eleq1d ⊢ ( 𝑡 = ∅ → ( ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵 ) ∈ Comp ↔ ( 𝐽 ↾t ∅ ) ∈ Comp ) )
10 4 9 imbi12d ⊢ ( 𝑡 = ∅ → ( ( 𝑡 ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵 ) ∈ Comp ) ↔ ( ∅ ⊆ 𝐴 → ( 𝐽 ↾t ∅ ) ∈ Comp ) ) )
11 10 imbi2d ⊢ ( 𝑡 = ∅ → ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) → ( 𝑡 ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵 ) ∈ Comp ) ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) → ( ∅ ⊆ 𝐴 → ( 𝐽 ↾t ∅ ) ∈ Comp ) ) ) )
12 sseq1 ⊢ ( 𝑡 = 𝑦 → ( 𝑡 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴 ) )
13 iuneq1 ⊢ ( 𝑡 = 𝑦 → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ 𝑦 𝐵 )
14 13 oveq2d ⊢ ( 𝑡 = 𝑦 → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵 ) = ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) )
15 14 eleq1d ⊢ ( 𝑡 = 𝑦 → ( ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵 ) ∈ Comp ↔ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) )
16 12 15 imbi12d ⊢ ( 𝑡 = 𝑦 → ( ( 𝑡 ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵 ) ∈ Comp ) ↔ ( 𝑦 ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) )
17 16 imbi2d ⊢ ( 𝑡 = 𝑦 → ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) → ( 𝑡 ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵 ) ∈ Comp ) ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) → ( 𝑦 ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) ) )
18 sseq1 ⊢ ( 𝑡 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑡 ⊆ 𝐴 ↔ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) )
19 iuneq1 ⊢ ( 𝑡 = ( 𝑦 ∪ { 𝑧 } ) → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 )
20 19 oveq2d ⊢ ( 𝑡 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵 ) = ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) )
21 20 eleq1d ⊢ ( 𝑡 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵 ) ∈ Comp ↔ ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ∈ Comp ) )
22 18 21 imbi12d ⊢ ( 𝑡 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝑡 ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵 ) ∈ Comp ) ↔ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ∈ Comp ) ) )
23 22 imbi2d ⊢ ( 𝑡 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) → ( 𝑡 ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵 ) ∈ Comp ) ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ∈ Comp ) ) ) )
24 sseq1 ⊢ ( 𝑡 = 𝐴 → ( 𝑡 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴 ) )
25 iuneq1 ⊢ ( 𝑡 = 𝐴 → ∪ 𝑥 ∈ 𝑡 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵 )
26 25 oveq2d ⊢ ( 𝑡 = 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵 ) = ( 𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵 ) )
27 26 eleq1d ⊢ ( 𝑡 = 𝐴 → ( ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵 ) ∈ Comp ↔ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵 ) ∈ Comp ) )
28 24 27 imbi12d ⊢ ( 𝑡 = 𝐴 → ( ( 𝑡 ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵 ) ∈ Comp ) ↔ ( 𝐴 ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵 ) ∈ Comp ) ) )
29 28 imbi2d ⊢ ( 𝑡 = 𝐴 → ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) → ( 𝑡 ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑡 𝐵 ) ∈ Comp ) ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) → ( 𝐴 ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵 ) ∈ Comp ) ) ) )
30 rest0 ⊢ ( 𝐽 ∈ Top → ( 𝐽 ↾t ∅ ) = { ∅ } )
31 0cmp ⊢ { ∅ } ∈ Comp
32 30 31 eqeltrdi ⊢ ( 𝐽 ∈ Top → ( 𝐽 ↾t ∅ ) ∈ Comp )
33 32 3ad2ant1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) → ( 𝐽 ↾t ∅ ) ∈ Comp )
34 33 a1d ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) → ( ∅ ⊆ 𝐴 → ( 𝐽 ↾t ∅ ) ∈ Comp ) )
35 ssun1 ⊢ 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } )
36 id ⊢ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 )
37 35 36 sstrid ⊢ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → 𝑦 ⊆ 𝐴 )
38 37 imim1i ⊢ ( ( 𝑦 ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) )
39 simpl1 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → 𝐽 ∈ Top )
40 iunxun ⊢ ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 = ( ∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ { 𝑧 } 𝐵 )
41 simprr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp )
42 cmptop ⊢ ( ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Top )
43 restrcl ⊢ ( ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Top → ( 𝐽 ∈ V ∧ ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V ) )
44 43 simprd ⊢ ( ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Top → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V )
45 41 42 44 3syl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V )
46 nfcv ⊢ Ⅎ 𝑡 𝐵
47 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑡 / 𝑥 ⦌ 𝐵
48 csbeq1a ⊢ ( 𝑥 = 𝑡 → 𝐵 = ⦋ 𝑡 / 𝑥 ⦌ 𝐵 )
49 46 47 48 cbviun ⊢ ∪ 𝑥 ∈ { 𝑧 } 𝐵 = ∪ 𝑡 ∈ { 𝑧 } ⦋ 𝑡 / 𝑥 ⦌ 𝐵
50 vex ⊢ 𝑧 ∈ V
51 csbeq1 ⊢ ( 𝑡 = 𝑧 → ⦋ 𝑡 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
52 50 51 iunxsn ⊢ ∪ 𝑡 ∈ { 𝑧 } ⦋ 𝑡 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵
53 49 52 eqtri ⊢ ∪ 𝑥 ∈ { 𝑧 } 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵
54 51 oveq2d ⊢ ( 𝑡 = 𝑧 → ( 𝐽 ↾t ⦋ 𝑡 / 𝑥 ⦌ 𝐵 ) = ( 𝐽 ↾t ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
55 54 eleq1d ⊢ ( 𝑡 = 𝑧 → ( ( 𝐽 ↾t ⦋ 𝑡 / 𝑥 ⦌ 𝐵 ) ∈ Comp ↔ ( 𝐽 ↾t ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∈ Comp ) )
56 simpl3 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp )
57 nfv ⊢ Ⅎ 𝑡 ( 𝐽 ↾t 𝐵 ) ∈ Comp
58 nfcv ⊢ Ⅎ 𝑥 𝐽
59 nfcv ⊢ Ⅎ 𝑥 ↾t
60 58 59 47 nfov ⊢ Ⅎ 𝑥 ( 𝐽 ↾t ⦋ 𝑡 / 𝑥 ⦌ 𝐵 )
61 60 nfel1 ⊢ Ⅎ 𝑥 ( 𝐽 ↾t ⦋ 𝑡 / 𝑥 ⦌ 𝐵 ) ∈ Comp
62 48 oveq2d ⊢ ( 𝑥 = 𝑡 → ( 𝐽 ↾t 𝐵 ) = ( 𝐽 ↾t ⦋ 𝑡 / 𝑥 ⦌ 𝐵 ) )
63 62 eleq1d ⊢ ( 𝑥 = 𝑡 → ( ( 𝐽 ↾t 𝐵 ) ∈ Comp ↔ ( 𝐽 ↾t ⦋ 𝑡 / 𝑥 ⦌ 𝐵 ) ∈ Comp ) )
64 57 61 63 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ↔ ∀ 𝑡 ∈ 𝐴 ( 𝐽 ↾t ⦋ 𝑡 / 𝑥 ⦌ 𝐵 ) ∈ Comp )
65 56 64 sylib ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ∀ 𝑡 ∈ 𝐴 ( 𝐽 ↾t ⦋ 𝑡 / 𝑥 ⦌ 𝐵 ) ∈ Comp )
66 ssun2 ⊢ { 𝑧 } ⊆ ( 𝑦 ∪ { 𝑧 } )
67 simprl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 )
68 66 67 sstrid ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → { 𝑧 } ⊆ 𝐴 )
69 50 snss ⊢ ( 𝑧 ∈ 𝐴 ↔ { 𝑧 } ⊆ 𝐴 )
70 68 69 sylibr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → 𝑧 ∈ 𝐴 )
71 55 65 70 rspcdva ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ( 𝐽 ↾t ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∈ Comp )
72 cmptop ⊢ ( ( 𝐽 ↾t ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∈ Comp → ( 𝐽 ↾t ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∈ Top )
73 restrcl ⊢ ( ( 𝐽 ↾t ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∈ Top → ( 𝐽 ∈ V ∧ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ V ) )
74 73 simprd ⊢ ( ( 𝐽 ↾t ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∈ Top → ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ V )
75 71 72 74 3syl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ V )
76 53 75 eqeltrid ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ∪ 𝑥 ∈ { 𝑧 } 𝐵 ∈ V )
77 unexg ⊢ ( ( ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V ∧ ∪ 𝑥 ∈ { 𝑧 } 𝐵 ∈ V ) → ( ∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ { 𝑧 } 𝐵 ) ∈ V )
78 45 76 77 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ( ∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ { 𝑧 } 𝐵 ) ∈ V )
79 40 78 eqeltrid ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ V )
80 resttop ⊢ ( ( 𝐽 ∈ Top ∧ ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ V ) → ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ∈ Top )
81 39 79 80 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ∈ Top )
82 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
83 82 restin ⊢ ( ( 𝐽 ∈ Top ∧ ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ V ) → ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = ( 𝐽 ↾t ( ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∩ ∪ 𝐽 ) ) )
84 39 79 83 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = ( 𝐽 ↾t ( ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∩ ∪ 𝐽 ) ) )
85 84 unieqd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ∪ ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = ∪ ( 𝐽 ↾t ( ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∩ ∪ 𝐽 ) ) )
86 inss2 ⊢ ( ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∩ ∪ 𝐽 ) ⊆ ∪ 𝐽
87 86 1 sseqtrri ⊢ ( ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∩ ∪ 𝐽 ) ⊆ 𝑋
88 1 restuni ⊢ ( ( 𝐽 ∈ Top ∧ ( ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∩ ∪ 𝐽 ) ⊆ 𝑋 ) → ( ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∩ ∪ 𝐽 ) = ∪ ( 𝐽 ↾t ( ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∩ ∪ 𝐽 ) ) )
89 39 87 88 sylancl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ( ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∩ ∪ 𝐽 ) = ∪ ( 𝐽 ↾t ( ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∩ ∪ 𝐽 ) ) )
90 85 89 eqtr4d ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ∪ ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = ( ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∩ ∪ 𝐽 ) )
91 53 uneq2i ⊢ ( ∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ { 𝑧 } 𝐵 ) = ( ∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
92 40 91 eqtri ⊢ ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 = ( ∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
93 92 ineq1i ⊢ ( ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∩ ∪ 𝐽 ) = ( ( ∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∩ ∪ 𝐽 )
94 indir ⊢ ( ( ∪ 𝑥 ∈ 𝑦 𝐵 ∪ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∩ ∪ 𝐽 ) = ( ( ∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽 ) ∪ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ∪ 𝐽 ) )
95 93 94 eqtri ⊢ ( ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∩ ∪ 𝐽 ) = ( ( ∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽 ) ∪ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ∪ 𝐽 ) )
96 90 95 eqtrdi ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ∪ ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = ( ( ∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽 ) ∪ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ∪ 𝐽 ) ) )
97 inss1 ⊢ ( ∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽 ) ⊆ ∪ 𝑥 ∈ 𝑦 𝐵
98 ssun1 ⊢ ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ { 𝑧 } 𝐵 )
99 98 40 sseqtrri ⊢ ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵
100 97 99 sstri ⊢ ( ∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽 ) ⊆ ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵
101 100 a1i ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ( ∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽 ) ⊆ ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 )
102 restabs ⊢ ( ( 𝐽 ∈ Top ∧ ( ∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽 ) ⊆ ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∧ ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ V ) → ( ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ↾t ( ∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽 ) ) = ( 𝐽 ↾t ( ∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽 ) ) )
103 39 101 79 102 syl3anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ( ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ↾t ( ∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽 ) ) = ( 𝐽 ↾t ( ∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽 ) ) )
104 82 restin ⊢ ( ( 𝐽 ∈ Top ∧ ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V ) → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) = ( 𝐽 ↾t ( ∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽 ) ) )
105 39 45 104 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) = ( 𝐽 ↾t ( ∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽 ) ) )
106 103 105 eqtr4d ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ( ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ↾t ( ∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽 ) ) = ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) )
107 106 41 eqeltrd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ( ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ↾t ( ∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽 ) ) ∈ Comp )
108 inss1 ⊢ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ∪ 𝐽 ) ⊆ ⦋ 𝑧 / 𝑥 ⦌ 𝐵
109 ssun2 ⊢ ∪ 𝑥 ∈ { 𝑧 } 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ { 𝑧 } 𝐵 )
110 109 40 sseqtrri ⊢ ∪ 𝑥 ∈ { 𝑧 } 𝐵 ⊆ ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵
111 53 110 eqsstrri ⊢ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ⊆ ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵
112 108 111 sstri ⊢ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ∪ 𝐽 ) ⊆ ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵
113 112 a1i ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ∪ 𝐽 ) ⊆ ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 )
114 restabs ⊢ ( ( 𝐽 ∈ Top ∧ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ∪ 𝐽 ) ⊆ ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∧ ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ V ) → ( ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ↾t ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ∪ 𝐽 ) ) = ( 𝐽 ↾t ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ∪ 𝐽 ) ) )
115 39 113 79 114 syl3anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ( ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ↾t ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ∪ 𝐽 ) ) = ( 𝐽 ↾t ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ∪ 𝐽 ) ) )
116 82 restin ⊢ ( ( 𝐽 ∈ Top ∧ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ V ) → ( 𝐽 ↾t ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ( 𝐽 ↾t ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ∪ 𝐽 ) ) )
117 39 75 116 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ( 𝐽 ↾t ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ( 𝐽 ↾t ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ∪ 𝐽 ) ) )
118 115 117 eqtr4d ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ( ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ↾t ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ∪ 𝐽 ) ) = ( 𝐽 ↾t ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
119 118 71 eqeltrd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ( ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ↾t ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ∪ 𝐽 ) ) ∈ Comp )
120 eqid ⊢ ∪ ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = ∪ ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 )
121 120 uncmp ⊢ ( ( ( ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ∈ Top ∧ ∪ ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = ( ( ∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽 ) ∪ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ∪ 𝐽 ) ) ) ∧ ( ( ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ↾t ( ∪ 𝑥 ∈ 𝑦 𝐵 ∩ ∪ 𝐽 ) ) ∈ Comp ∧ ( ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ↾t ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ∪ 𝐽 ) ) ∈ Comp ) ) → ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ∈ Comp )
122 81 96 107 119 121 syl22anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ∈ Comp )
123 122 exp32 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp → ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ∈ Comp ) ) )
124 123 a2d ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) → ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ∈ Comp ) ) )
125 38 124 syl5 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) → ( ( 𝑦 ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ∈ Comp ) ) )
126 125 a2i ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) → ( 𝑦 ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ∈ Comp ) ) )
127 126 a1i ⊢ ( 𝑦 ∈ Fin → ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) → ( 𝑦 ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝑦 𝐵 ) ∈ Comp ) ) → ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) ∈ Comp ) ) ) )
128 11 17 23 29 34 127 findcard2 ⊢ ( 𝐴 ∈ Fin → ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) → ( 𝐴 ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵 ) ∈ Comp ) ) )
129 3 128 mpcom ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) → ( 𝐴 ⊆ 𝐴 → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵 ) ∈ Comp ) )
130 2 129 mpi ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐽 ↾t 𝐵 ) ∈ Comp ) → ( 𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵 ) ∈ Comp )