Metamath Proof Explorer

Theorem mclsind

Description: Induction theorem for closure: any other set Q closed under the axioms and the hypotheses contains all the elements of the closure. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mclsval.d 
|- D = ( mDV ` T )
mclsval.e 
|- E = ( mEx ` T )
mclsval.c 
|- C = ( mCls ` T )
mclsval.1 
|- ( ph -> T e. mFS )
mclsval.2 
|- ( ph -> K C_ D )
mclsval.3 
|- ( ph -> B C_ E )
mclsax.a 
|- A = ( mAx ` T )
mclsax.l 
|- L = ( mSubst ` T )
mclsax.v 
|- V = ( mVR ` T )
mclsax.h 
|- H = ( mVH ` T )
mclsax.w 
|- W = ( mVars ` T )
mclsind.4 
|- ( ph -> B C_ Q )
mclsind.5 
|- ( ( ph /\ v e. V ) -> ( H ` v ) e. Q )
mclsind.6 
|- ( ( ph /\ ( <. m , o , p >. e. A /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ Q ) /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. Q )
Assertion mclsind 
|- ( ph -> ( K C B ) C_ Q )

Proof

Step Hyp Ref Expression
1 mclsval.d 
 |-  D = ( mDV ` T )
2 mclsval.e 
 |-  E = ( mEx ` T )
3 mclsval.c 
 |-  C = ( mCls ` T )
4 mclsval.1 
 |-  ( ph -> T e. mFS )
5 mclsval.2 
 |-  ( ph -> K C_ D )
6 mclsval.3 
 |-  ( ph -> B C_ E )
7 mclsax.a 
 |-  A = ( mAx ` T )
8 mclsax.l 
 |-  L = ( mSubst ` T )
9 mclsax.v 
 |-  V = ( mVR ` T )
10 mclsax.h 
 |-  H = ( mVH ` T )
11 mclsax.w 
 |-  W = ( mVars ` T )
12 mclsind.4 
 |-  ( ph -> B C_ Q )
13 mclsind.5 
 |-  ( ( ph /\ v e. V ) -> ( H ` v ) e. Q )
14 mclsind.6 
 |-  ( ( ph /\ ( <. m , o , p >. e. A /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ Q ) /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. Q )
15 1 2 3 4 5 6 10 7 8 11 mclsval 
 |-  ( ph -> ( K C B ) = |^| { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran L ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } )
16 6 12 ssind 
 |-  ( ph -> B C_ ( E i^i Q ) )
17 9 2 10 mvhf 
 |-  ( T e. mFS -> H : V --> E )
18 4 17 syl 
 |-  ( ph -> H : V --> E )
19 18 ffnd 
 |-  ( ph -> H Fn V )
20 18 ffvelrnda 
 |-  ( ( ph /\ v e. V ) -> ( H ` v ) e. E )
21 20 13 elind 
 |-  ( ( ph /\ v e. V ) -> ( H ` v ) e. ( E i^i Q ) )
22 21 ralrimiva 
 |-  ( ph -> A. v e. V ( H ` v ) e. ( E i^i Q ) )
23 ffnfv 
 |-  ( H : V --> ( E i^i Q ) <-> ( H Fn V /\ A. v e. V ( H ` v ) e. ( E i^i Q ) ) )
24 19 22 23 sylanbrc 
 |-  ( ph -> H : V --> ( E i^i Q ) )
25 24 frnd 
 |-  ( ph -> ran H C_ ( E i^i Q ) )
26 16 25 unssd 
 |-  ( ph -> ( B u. ran H ) C_ ( E i^i Q ) )
27 id 
 |-  ( ( s " ( o u. ran H ) ) C_ ( E i^i Q ) -> ( s " ( o u. ran H ) ) C_ ( E i^i Q ) )
28 inss2 
 |-  ( E i^i Q ) C_ Q
29 27 28 sstrdi 
 |-  ( ( s " ( o u. ran H ) ) C_ ( E i^i Q ) -> ( s " ( o u. ran H ) ) C_ Q )
30 4 adantr 
 |-  ( ( ph /\ ( <. m , o , p >. e. A /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ Q ) ) -> T e. mFS )
31 eqid 
 |-  ( mREx ` T ) = ( mREx ` T )
32 9 31 8 2 msubff 
 |-  ( T e. mFS -> L : ( ( mREx ` T ) ^pm V ) --> ( E ^m E ) )
33 frn 
 |-  ( L : ( ( mREx ` T ) ^pm V ) --> ( E ^m E ) -> ran L C_ ( E ^m E ) )
34 30 32 33 3syl 
 |-  ( ( ph /\ ( <. m , o , p >. e. A /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ Q ) ) -> ran L C_ ( E ^m E ) )
35 simpr2 
 |-  ( ( ph /\ ( <. m , o , p >. e. A /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ Q ) ) -> s e. ran L )
36 34 35 sseldd 
 |-  ( ( ph /\ ( <. m , o , p >. e. A /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ Q ) ) -> s e. ( E ^m E ) )
37 elmapi 
 |-  ( s e. ( E ^m E ) -> s : E --> E )
38 36 37 syl 
 |-  ( ( ph /\ ( <. m , o , p >. e. A /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ Q ) ) -> s : E --> E )
39 eqid 
 |-  ( mStat ` T ) = ( mStat ` T )
40 7 39 maxsta 
 |-  ( T e. mFS -> A C_ ( mStat ` T ) )
41 30 40 syl 
 |-  ( ( ph /\ ( <. m , o , p >. e. A /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ Q ) ) -> A C_ ( mStat ` T ) )
42 eqid 
 |-  ( mPreSt ` T ) = ( mPreSt ` T )
43 42 39 mstapst 
 |-  ( mStat ` T ) C_ ( mPreSt ` T )
44 41 43 sstrdi 
 |-  ( ( ph /\ ( <. m , o , p >. e. A /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ Q ) ) -> A C_ ( mPreSt ` T ) )
45 simpr1 
 |-  ( ( ph /\ ( <. m , o , p >. e. A /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ Q ) ) -> <. m , o , p >. e. A )
46 44 45 sseldd 
 |-  ( ( ph /\ ( <. m , o , p >. e. A /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ Q ) ) -> <. m , o , p >. e. ( mPreSt ` T ) )
47 1 2 42 elmpst 
 |-  ( <. m , o , p >. e. ( mPreSt ` T ) <-> ( ( m C_ D /\ `' m = m ) /\ ( o C_ E /\ o e. Fin ) /\ p e. E ) )
48 47 simp3bi 
 |-  ( <. m , o , p >. e. ( mPreSt ` T ) -> p e. E )
49 46 48 syl 
 |-  ( ( ph /\ ( <. m , o , p >. e. A /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ Q ) ) -> p e. E )
50 38 49 ffvelrnd 
 |-  ( ( ph /\ ( <. m , o , p >. e. A /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ Q ) ) -> ( s ` p ) e. E )
51 50 3adant3 
 |-  ( ( ph /\ ( <. m , o , p >. e. A /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ Q ) /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. E )
52 51 14 elind 
 |-  ( ( ph /\ ( <. m , o , p >. e. A /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ Q ) /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. ( E i^i Q ) )
53 52 3exp 
 |-  ( ph -> ( ( <. m , o , p >. e. A /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ Q ) -> ( A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) -> ( s ` p ) e. ( E i^i Q ) ) ) )
54 53 3expd 
 |-  ( ph -> ( <. m , o , p >. e. A -> ( s e. ran L -> ( ( s " ( o u. ran H ) ) C_ Q -> ( A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) -> ( s ` p ) e. ( E i^i Q ) ) ) ) ) )
55 54 imp31 
 |-  ( ( ( ph /\ <. m , o , p >. e. A ) /\ s e. ran L ) -> ( ( s " ( o u. ran H ) ) C_ Q -> ( A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) -> ( s ` p ) e. ( E i^i Q ) ) ) )
56 29 55 syl5 
 |-  ( ( ( ph /\ <. m , o , p >. e. A ) /\ s e. ran L ) -> ( ( s " ( o u. ran H ) ) C_ ( E i^i Q ) -> ( A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) -> ( s ` p ) e. ( E i^i Q ) ) ) )
57 56 impd 
 |-  ( ( ( ph /\ <. m , o , p >. e. A ) /\ s e. ran L ) -> ( ( ( s " ( o u. ran H ) ) C_ ( E i^i Q ) /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. ( E i^i Q ) ) )
58 57 ralrimiva 
 |-  ( ( ph /\ <. m , o , p >. e. A ) -> A. s e. ran L ( ( ( s " ( o u. ran H ) ) C_ ( E i^i Q ) /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. ( E i^i Q ) ) )
59 58 ex 
 |-  ( ph -> ( <. m , o , p >. e. A -> A. s e. ran L ( ( ( s " ( o u. ran H ) ) C_ ( E i^i Q ) /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. ( E i^i Q ) ) ) )
60 59 alrimiv 
 |-  ( ph -> A. p ( <. m , o , p >. e. A -> A. s e. ran L ( ( ( s " ( o u. ran H ) ) C_ ( E i^i Q ) /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. ( E i^i Q ) ) ) )
61 60 alrimivv 
 |-  ( ph -> A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran L ( ( ( s " ( o u. ran H ) ) C_ ( E i^i Q ) /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. ( E i^i Q ) ) ) )
62 2 fvexi 
 |-  E e. _V
63 62 inex1 
 |-  ( E i^i Q ) e. _V
64 sseq2 
 |-  ( c = ( E i^i Q ) -> ( ( B u. ran H ) C_ c <-> ( B u. ran H ) C_ ( E i^i Q ) ) )
65 sseq2 
 |-  ( c = ( E i^i Q ) -> ( ( s " ( o u. ran H ) ) C_ c <-> ( s " ( o u. ran H ) ) C_ ( E i^i Q ) ) )
66 65 anbi1d 
 |-  ( c = ( E i^i Q ) -> ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) <-> ( ( s " ( o u. ran H ) ) C_ ( E i^i Q ) /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) ) )
67 eleq2 
 |-  ( c = ( E i^i Q ) -> ( ( s ` p ) e. c <-> ( s ` p ) e. ( E i^i Q ) ) )
68 66 67 imbi12d 
 |-  ( c = ( E i^i Q ) -> ( ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) <-> ( ( ( s " ( o u. ran H ) ) C_ ( E i^i Q ) /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. ( E i^i Q ) ) ) )
69 68 ralbidv 
 |-  ( c = ( E i^i Q ) -> ( A. s e. ran L ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) <-> A. s e. ran L ( ( ( s " ( o u. ran H ) ) C_ ( E i^i Q ) /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. ( E i^i Q ) ) ) )
70 69 imbi2d 
 |-  ( c = ( E i^i Q ) -> ( ( <. m , o , p >. e. A -> A. s e. ran L ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) <-> ( <. m , o , p >. e. A -> A. s e. ran L ( ( ( s " ( o u. ran H ) ) C_ ( E i^i Q ) /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. ( E i^i Q ) ) ) ) )
71 70 albidv 
 |-  ( c = ( E i^i Q ) -> ( A. p ( <. m , o , p >. e. A -> A. s e. ran L ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) <-> A. p ( <. m , o , p >. e. A -> A. s e. ran L ( ( ( s " ( o u. ran H ) ) C_ ( E i^i Q ) /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. ( E i^i Q ) ) ) ) )
72 71 2albidv 
 |-  ( c = ( E i^i Q ) -> ( A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran L ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) <-> A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran L ( ( ( s " ( o u. ran H ) ) C_ ( E i^i Q ) /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. ( E i^i Q ) ) ) ) )
73 64 72 anbi12d 
 |-  ( c = ( E i^i Q ) -> ( ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran L ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) <-> ( ( B u. ran H ) C_ ( E i^i Q ) /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran L ( ( ( s " ( o u. ran H ) ) C_ ( E i^i Q ) /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. ( E i^i Q ) ) ) ) ) )
74 63 73 elab 
 |-  ( ( E i^i Q ) e. { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran L ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } <-> ( ( B u. ran H ) C_ ( E i^i Q ) /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran L ( ( ( s " ( o u. ran H ) ) C_ ( E i^i Q ) /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. ( E i^i Q ) ) ) ) )
75 26 61 74 sylanbrc 
 |-  ( ph -> ( E i^i Q ) e. { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran L ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } )
76 intss1 
 |-  ( ( E i^i Q ) e. { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran L ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } -> |^| { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran L ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } C_ ( E i^i Q ) )
77 75 76 syl 
 |-  ( ph -> |^| { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran L ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } C_ ( E i^i Q ) )
78 77 28 sstrdi 
 |-  ( ph -> |^| { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran L ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } C_ Q )
79 15 78 eqsstrd 
 |-  ( ph -> ( K C B ) C_ Q )