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 )