Metamath Proof Explorer

Theorem grumnudlem

Description: Lemma for grumnud . (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypotheses grumnudlem.1 
|- M = { k | A. l e. k ( ~P l C_ k /\ A. m E. n e. k ( ~P l C_ n /\ A. p e. l ( E. q e. k ( p e. q /\ q e. m ) -> E. r e. m ( p e. r /\ U. r C_ n ) ) ) ) }
grumnudlem.2 
|- ( ph -> G e. Univ )
grumnudlem.3 
|- F = ( { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } i^i ( G X. G ) )
grumnudlem.4 
|- ( ( i e. G /\ h e. G ) -> ( i F h <-> E. j ( U. j = h /\ j e. f /\ i e. j ) ) )
grumnudlem.5 
|- ( ( h e. ( F Coll z ) /\ ( U. j = h /\ j e. f /\ i e. j ) ) -> E. u e. f ( i e. u /\ U. u e. ( F Coll z ) ) )
Assertion grumnudlem 
|- ( ph -> G e. M )

Proof

Step Hyp Ref Expression
1 grumnudlem.1 
 |-  M = { k | A. l e. k ( ~P l C_ k /\ A. m E. n e. k ( ~P l C_ n /\ A. p e. l ( E. q e. k ( p e. q /\ q e. m ) -> E. r e. m ( p e. r /\ U. r C_ n ) ) ) ) }
2 grumnudlem.2 
 |-  ( ph -> G e. Univ )
3 grumnudlem.3 
 |-  F = ( { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } i^i ( G X. G ) )
4 grumnudlem.4 
 |-  ( ( i e. G /\ h e. G ) -> ( i F h <-> E. j ( U. j = h /\ j e. f /\ i e. j ) ) )
5 grumnudlem.5 
 |-  ( ( h e. ( F Coll z ) /\ ( U. j = h /\ j e. f /\ i e. j ) ) -> E. u e. f ( i e. u /\ U. u e. ( F Coll z ) ) )
6 gruss 
 |-  ( ( G e. Univ /\ z e. G /\ a C_ z ) -> a e. G )
7 2 6 syl3an1 
 |-  ( ( ph /\ z e. G /\ a C_ z ) -> a e. G )
8 7 3expia 
 |-  ( ( ph /\ z e. G ) -> ( a C_ z -> a e. G ) )
9 8 alrimiv 
 |-  ( ( ph /\ z e. G ) -> A. a ( a C_ z -> a e. G ) )
10 pwss 
 |-  ( ~P z C_ G <-> A. a ( a C_ z -> a e. G ) )
11 9 10 sylibr 
 |-  ( ( ph /\ z e. G ) -> ~P z C_ G )
12 ssun1 
 |-  ~P z C_ ( ~P z u. U. ( F Coll z ) )
13 simp3 
 |-  ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) -> w = ( ~P z u. U. ( F Coll z ) ) )
14 12 13 sseqtrrid 
 |-  ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) -> ~P z C_ w )
15 simp1l3 
 |-  ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) -> w = ( ~P z u. U. ( F Coll z ) ) )
16 simp1r 
 |-  ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) -> i e. z )
17 simpr 
 |-  ( ( h = U. v /\ j = v ) -> j = v )
18 17 unieqd 
 |-  ( ( h = U. v /\ j = v ) -> U. j = U. v )
19 simpl 
 |-  ( ( h = U. v /\ j = v ) -> h = U. v )
20 18 19 eqtr4d 
 |-  ( ( h = U. v /\ j = v ) -> U. j = h )
21 20 adantll 
 |-  ( ( ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) /\ h = U. v ) /\ j = v ) -> U. j = h )
22 simpr 
 |-  ( ( ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) /\ h = U. v ) /\ j = v ) -> j = v )
23 simpll3 
 |-  ( ( ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) /\ h = U. v ) /\ j = v ) -> ( i e. v /\ v e. f ) )
24 23 simprd 
 |-  ( ( ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) /\ h = U. v ) /\ j = v ) -> v e. f )
25 22 24 eqeltrd 
 |-  ( ( ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) /\ h = U. v ) /\ j = v ) -> j e. f )
26 23 simpld 
 |-  ( ( ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) /\ h = U. v ) /\ j = v ) -> i e. v )
27 26 22 eleqtrrd 
 |-  ( ( ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) /\ h = U. v ) /\ j = v ) -> i e. j )
28 21 25 27 3jca 
 |-  ( ( ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) /\ h = U. v ) /\ j = v ) -> ( U. j = h /\ j e. f /\ i e. j ) )
29 simpl2 
 |-  ( ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) /\ h = U. v ) -> v e. G )
30 28 29 rr-spce 
 |-  ( ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) /\ h = U. v ) -> E. j ( U. j = h /\ j e. f /\ i e. j ) )
31 simp1l1 
 |-  ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) -> ph )
32 31 2 syl 
 |-  ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) -> G e. Univ )
33 simp2 
 |-  ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) -> v e. G )
34 gruuni 
 |-  ( ( G e. Univ /\ v e. G ) -> U. v e. G )
35 32 33 34 syl2anc 
 |-  ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) -> U. v e. G )
36 30 35 rspcime 
 |-  ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) -> E. h e. G E. j ( U. j = h /\ j e. f /\ i e. j ) )
37 simpl1 
 |-  ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) -> ph )
38 37 2 syl 
 |-  ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) -> G e. Univ )
39 simpl2 
 |-  ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) -> z e. G )
40 simpr 
 |-  ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) -> i e. z )
41 gruel 
 |-  ( ( G e. Univ /\ z e. G /\ i e. z ) -> i e. G )
42 38 39 40 41 syl3anc 
 |-  ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) -> i e. G )
43 42 3ad2ant1 
 |-  ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) -> i e. G )
44 43 4 sylan 
 |-  ( ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) /\ h e. G ) -> ( i F h <-> E. j ( U. j = h /\ j e. f /\ i e. j ) ) )
45 44 rexbidva 
 |-  ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) -> ( E. h e. G i F h <-> E. h e. G E. j ( U. j = h /\ j e. f /\ i e. j ) ) )
46 36 45 mpbird 
 |-  ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) -> E. h e. G i F h )
47 rexex 
 |-  ( E. h e. G i F h -> E. h i F h )
48 46 47 syl 
 |-  ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) -> E. h i F h )
49 16 48 cpcoll2d 
 |-  ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) -> E. h e. ( F Coll z ) i F h )
50 32 adantr 
 |-  ( ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) /\ h e. ( F Coll z ) ) -> G e. Univ )
51 39 3ad2ant1 
 |-  ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) -> z e. G )
52 51 adantr 
 |-  ( ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) /\ h e. ( F Coll z ) ) -> z e. G )
53 2 adantr 
 |-  ( ( ph /\ z e. G ) -> G e. Univ )
54 inss2 
 |-  ( { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } i^i ( G X. G ) ) C_ ( G X. G )
55 3 54 eqsstri 
 |-  F C_ ( G X. G )
56 55 a1i 
 |-  ( ( ph /\ z e. G ) -> F C_ ( G X. G ) )
57 simpr 
 |-  ( ( ph /\ z e. G ) -> z e. G )
58 53 56 57 grucollcld 
 |-  ( ( ph /\ z e. G ) -> ( F Coll z ) e. G )
59 31 52 58 syl2an2r 
 |-  ( ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) /\ h e. ( F Coll z ) ) -> ( F Coll z ) e. G )
60 simpr 
 |-  ( ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) /\ h e. ( F Coll z ) ) -> h e. ( F Coll z ) )
61 gruel 
 |-  ( ( G e. Univ /\ ( F Coll z ) e. G /\ h e. ( F Coll z ) ) -> h e. G )
62 50 59 60 61 syl3anc 
 |-  ( ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) /\ h e. ( F Coll z ) ) -> h e. G )
63 43 62 4 syl2an2r 
 |-  ( ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) /\ h e. ( F Coll z ) ) -> ( i F h <-> E. j ( U. j = h /\ j e. f /\ i e. j ) ) )
64 63 rexbidva 
 |-  ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) -> ( E. h e. ( F Coll z ) i F h <-> E. h e. ( F Coll z ) E. j ( U. j = h /\ j e. f /\ i e. j ) ) )
65 49 64 mpbid 
 |-  ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) -> E. h e. ( F Coll z ) E. j ( U. j = h /\ j e. f /\ i e. j ) )
66 rexcom4 
 |-  ( E. h e. ( F Coll z ) E. j ( U. j = h /\ j e. f /\ i e. j ) <-> E. j E. h e. ( F Coll z ) ( U. j = h /\ j e. f /\ i e. j ) )
67 5 rexlimiva 
 |-  ( E. h e. ( F Coll z ) ( U. j = h /\ j e. f /\ i e. j ) -> E. u e. f ( i e. u /\ U. u e. ( F Coll z ) ) )
68 67 exlimiv 
 |-  ( E. j E. h e. ( F Coll z ) ( U. j = h /\ j e. f /\ i e. j ) -> E. u e. f ( i e. u /\ U. u e. ( F Coll z ) ) )
69 66 68 sylbi 
 |-  ( E. h e. ( F Coll z ) E. j ( U. j = h /\ j e. f /\ i e. j ) -> E. u e. f ( i e. u /\ U. u e. ( F Coll z ) ) )
70 65 69 syl 
 |-  ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) -> E. u e. f ( i e. u /\ U. u e. ( F Coll z ) ) )
71 elssuni 
 |-  ( U. u e. ( F Coll z ) -> U. u C_ U. ( F Coll z ) )
72 ssun2 
 |-  U. ( F Coll z ) C_ ( ~P z u. U. ( F Coll z ) )
73 71 72 sstrdi 
 |-  ( U. u e. ( F Coll z ) -> U. u C_ ( ~P z u. U. ( F Coll z ) ) )
74 73 adantl 
 |-  ( ( w = ( ~P z u. U. ( F Coll z ) ) /\ U. u e. ( F Coll z ) ) -> U. u C_ ( ~P z u. U. ( F Coll z ) ) )
75 simpl 
 |-  ( ( w = ( ~P z u. U. ( F Coll z ) ) /\ U. u e. ( F Coll z ) ) -> w = ( ~P z u. U. ( F Coll z ) ) )
76 74 75 sseqtrrd 
 |-  ( ( w = ( ~P z u. U. ( F Coll z ) ) /\ U. u e. ( F Coll z ) ) -> U. u C_ w )
77 76 ex 
 |-  ( w = ( ~P z u. U. ( F Coll z ) ) -> ( U. u e. ( F Coll z ) -> U. u C_ w ) )
78 77 anim2d 
 |-  ( w = ( ~P z u. U. ( F Coll z ) ) -> ( ( i e. u /\ U. u e. ( F Coll z ) ) -> ( i e. u /\ U. u C_ w ) ) )
79 78 reximdv 
 |-  ( w = ( ~P z u. U. ( F Coll z ) ) -> ( E. u e. f ( i e. u /\ U. u e. ( F Coll z ) ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) )
80 15 70 79 sylc 
 |-  ( ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) /\ v e. G /\ ( i e. v /\ v e. f ) ) -> E. u e. f ( i e. u /\ U. u C_ w ) )
81 80 rexlimdv3a 
 |-  ( ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) /\ i e. z ) -> ( E. v e. G ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) )
82 81 ralrimiva 
 |-  ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) -> A. i e. z ( E. v e. G ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) )
83 14 82 jca 
 |-  ( ( ph /\ z e. G /\ w = ( ~P z u. U. ( F Coll z ) ) ) -> ( ~P z C_ w /\ A. i e. z ( E. v e. G ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) )
84 83 3expa 
 |-  ( ( ( ph /\ z e. G ) /\ w = ( ~P z u. U. ( F Coll z ) ) ) -> ( ~P z C_ w /\ A. i e. z ( E. v e. G ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) )
85 grupw 
 |-  ( ( G e. Univ /\ z e. G ) -> ~P z e. G )
86 2 85 sylan 
 |-  ( ( ph /\ z e. G ) -> ~P z e. G )
87 gruuni 
 |-  ( ( G e. Univ /\ ( F Coll z ) e. G ) -> U. ( F Coll z ) e. G )
88 2 58 87 syl2an2r 
 |-  ( ( ph /\ z e. G ) -> U. ( F Coll z ) e. G )
89 gruun 
 |-  ( ( G e. Univ /\ ~P z e. G /\ U. ( F Coll z ) e. G ) -> ( ~P z u. U. ( F Coll z ) ) e. G )
90 53 86 88 89 syl3anc 
 |-  ( ( ph /\ z e. G ) -> ( ~P z u. U. ( F Coll z ) ) e. G )
91 84 90 rspcime 
 |-  ( ( ph /\ z e. G ) -> E. w e. G ( ~P z C_ w /\ A. i e. z ( E. v e. G ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) )
92 91 alrimiv 
 |-  ( ( ph /\ z e. G ) -> A. f E. w e. G ( ~P z C_ w /\ A. i e. z ( E. v e. G ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) )
93 11 92 jca 
 |-  ( ( ph /\ z e. G ) -> ( ~P z C_ G /\ A. f E. w e. G ( ~P z C_ w /\ A. i e. z ( E. v e. G ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) )
94 93 ralrimiva 
 |-  ( ph -> A. z e. G ( ~P z C_ G /\ A. f E. w e. G ( ~P z C_ w /\ A. i e. z ( E. v e. G ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) )
95 1 ismnu 
 |-  ( G e. Univ -> ( G e. M <-> A. z e. G ( ~P z C_ G /\ A. f E. w e. G ( ~P z C_ w /\ A. i e. z ( E. v e. G ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) ) )
96 2 95 syl 
 |-  ( ph -> ( G e. M <-> A. z e. G ( ~P z C_ G /\ A. f E. w e. G ( ~P z C_ w /\ A. i e. z ( E. v e. G ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) ) )
97 94 96 mpbird 
 |-  ( ph -> G e. M )