This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- X = U. J
Assertion fiuncmp 
|- ( ( J e. Top /\ A e. Fin /\ A. x e. A ( J |`t B ) e. Comp ) -> ( J |`t U_ x e. A B ) e. Comp )

Proof

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