Metamath Proof Explorer

Theorem unitscyglem3

Description: Lemma for unitscyg . (Contributed by metakunt, 14-Jul-2025)

Ref Expression
Hypotheses unitscyglem1.1 
|- B = ( Base ` G )
unitscyglem1.2 
|- .^ = ( .g ` G )
unitscyglem1.3 
|- ( ph -> G e. Grp )
unitscyglem1.4 
|- ( ph -> B e. Fin )
unitscyglem1.5 
|- ( ph -> A. n e. NN ( # ` { x e. B | ( n .^ x ) = ( 0g ` G ) } ) <_ n )
Assertion unitscyglem3 
|- ( ph -> A. d e. NN ( ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) ) )

Proof

Step Hyp Ref Expression
1 unitscyglem1.1 
 |-  B = ( Base ` G )
2 unitscyglem1.2 
 |-  .^ = ( .g ` G )
3 unitscyglem1.3 
 |-  ( ph -> G e. Grp )
4 unitscyglem1.4 
 |-  ( ph -> B e. Fin )
5 unitscyglem1.5 
 |-  ( ph -> A. n e. NN ( # ` { x e. B | ( n .^ x ) = ( 0g ` G ) } ) <_ n )
6 breq1 
 |-  ( d = c -> ( d || ( # ` B ) <-> c || ( # ` B ) ) )
7 eqeq2 
 |-  ( d = c -> ( ( ( od ` G ) ` x ) = d <-> ( ( od ` G ) ` x ) = c ) )
8 7 rabbidv 
 |-  ( d = c -> { x e. B | ( ( od ` G ) ` x ) = d } = { x e. B | ( ( od ` G ) ` x ) = c } )
9 8 neeq1d 
 |-  ( d = c -> ( { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) <-> { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) )
10 6 9 anbi12d 
 |-  ( d = c -> ( ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) <-> ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) ) )
11 8 fveq2d 
 |-  ( d = c -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) )
12 fveq2 
 |-  ( d = c -> ( phi ` d ) = ( phi ` c ) )
13 11 12 eqeq12d 
 |-  ( d = c -> ( ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) <-> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) )
14 10 13 imbi12d 
 |-  ( d = c -> ( ( ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) ) <-> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) )
15 14 imbi2d 
 |-  ( d = c -> ( ( ph -> ( ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) ) ) <-> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) )
16 simplr 
 |-  ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) -> ph )
17 simplll 
 |-  ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) -> d e. NN )
18 16 17 jca 
 |-  ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) -> ( ph /\ d e. NN ) )
19 breq1 
 |-  ( c = e -> ( c < d <-> e < d ) )
20 breq1 
 |-  ( c = e -> ( c || ( # ` B ) <-> e || ( # ` B ) ) )
21 eqeq2 
 |-  ( c = e -> ( ( ( od ` G ) ` x ) = c <-> ( ( od ` G ) ` x ) = e ) )
22 21 rabbidv 
 |-  ( c = e -> { x e. B | ( ( od ` G ) ` x ) = c } = { x e. B | ( ( od ` G ) ` x ) = e } )
23 22 neeq1d 
 |-  ( c = e -> ( { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) <-> { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) )
24 20 23 anbi12d 
 |-  ( c = e -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) <-> ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) ) )
25 22 fveq2d 
 |-  ( c = e -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) )
26 fveq2 
 |-  ( c = e -> ( phi ` c ) = ( phi ` e ) )
27 25 26 eqeq12d 
 |-  ( c = e -> ( ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) <-> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) )
28 24 27 imbi12d 
 |-  ( c = e -> ( ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) <-> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) )
29 28 imbi2d 
 |-  ( c = e -> ( ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) <-> ( ph -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) ) )
30 19 29 imbi12d 
 |-  ( c = e -> ( ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) <-> ( e < d -> ( ph -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) ) ) )
31 simpr 
 |-  ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) -> A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) )
32 31 adantr 
 |-  ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) -> A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) )
33 32 adantr 
 |-  ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) -> A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) )
34 33 adantr 
 |-  ( ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) /\ e e. NN ) -> A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) )
35 simpr 
 |-  ( ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) /\ e e. NN ) -> e e. NN )
36 30 34 35 rspcdva 
 |-  ( ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) /\ e e. NN ) -> ( e < d -> ( ph -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) ) )
37 simp-5r 
 |-  ( ( ( ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) /\ e e. NN ) /\ ( e < d -> ( ph -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) ) ) /\ e < d ) -> ph )
38 simpr 
 |-  ( ( ( ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) /\ e e. NN ) /\ ( e < d -> ( ph -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) ) ) /\ e < d ) -> e < d )
39 simplr 
 |-  ( ( ( ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) /\ e e. NN ) /\ ( e < d -> ( ph -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) ) ) /\ e < d ) -> ( e < d -> ( ph -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) ) )
40 38 39 mpd 
 |-  ( ( ( ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) /\ e e. NN ) /\ ( e < d -> ( ph -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) ) ) /\ e < d ) -> ( ph -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) )
41 37 40 mpd 
 |-  ( ( ( ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) /\ e e. NN ) /\ ( e < d -> ( ph -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) ) ) /\ e < d ) -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) )
42 41 ex 
 |-  ( ( ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) /\ e e. NN ) /\ ( e < d -> ( ph -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) ) ) -> ( e < d -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) )
43 42 ex 
 |-  ( ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) /\ e e. NN ) -> ( ( e < d -> ( ph -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) ) -> ( e < d -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) ) )
44 36 43 mpd 
 |-  ( ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) /\ e e. NN ) -> ( e < d -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) )
45 44 ralrimiva 
 |-  ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) -> A. e e. NN ( e < d -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) )
46 nfv 
 |-  F/ c ( e < d -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) )
47 nfv 
 |-  F/ e ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) )
48 breq1 
 |-  ( e = c -> ( e < d <-> c < d ) )
49 breq1 
 |-  ( e = c -> ( e || ( # ` B ) <-> c || ( # ` B ) ) )
50 eqeq2 
 |-  ( e = c -> ( ( ( od ` G ) ` x ) = e <-> ( ( od ` G ) ` x ) = c ) )
51 50 rabbidv 
 |-  ( e = c -> { x e. B | ( ( od ` G ) ` x ) = e } = { x e. B | ( ( od ` G ) ` x ) = c } )
52 51 neeq1d 
 |-  ( e = c -> ( { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) <-> { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) )
53 49 52 anbi12d 
 |-  ( e = c -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) <-> ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) ) )
54 51 fveq2d 
 |-  ( e = c -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) )
55 fveq2 
 |-  ( e = c -> ( phi ` e ) = ( phi ` c ) )
56 54 55 eqeq12d 
 |-  ( e = c -> ( ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) <-> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) )
57 53 56 imbi12d 
 |-  ( e = c -> ( ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) <-> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) )
58 48 57 imbi12d 
 |-  ( e = c -> ( ( e < d -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) <-> ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) )
59 46 47 58 cbvralw 
 |-  ( A. e e. NN ( e < d -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) <-> A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) )
60 59 biimpi 
 |-  ( A. e e. NN ( e < d -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) -> A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) )
61 45 60 syl 
 |-  ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) -> A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) )
62 18 61 jca 
 |-  ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) -> ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) )
63 simprl 
 |-  ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) -> d || ( # ` B ) )
64 62 63 jca 
 |-  ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) -> ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) )
65 simprr 
 |-  ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) -> { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) )
66 64 65 jca 
 |-  ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) -> ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) )
67 rabn0 
 |-  ( { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) <-> E. x e. B ( ( od ` G ) ` x ) = d )
68 67 bilani 
 |-  ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> E. x e. B ( ( od ` G ) ` x ) = d )
69 simp-4l 
 |-  ( ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ E. x e. B ( ( od ` G ) ` x ) = d ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) )
70 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ E. x e. B ( ( od ` G ) ` x ) = d ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> d || ( # ` B ) )
71 simplr 
 |-  ( ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ E. x e. B ( ( od ` G ) ` x ) = d ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> a e. B )
72 69 70 71 jca31 
 |-  ( ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ E. x e. B ( ( od ` G ) ` x ) = d ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) )
73 simpr 
 |-  ( ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ E. x e. B ( ( od ` G ) ` x ) = d ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> ( ( od ` G ) ` a ) = d )
74 72 73 jca 
 |-  ( ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ E. x e. B ( ( od ` G ) ` x ) = d ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) )
75 nfcv 
 |-  F/_ x B
76 nfcv 
 |-  F/_ z B
77 nfv 
 |-  F/ z ( ( od ` G ) ` x ) = d
78 nfv 
 |-  F/ x ( ( od ` G ) ` z ) = d
79 fveqeq2 
 |-  ( x = z -> ( ( ( od ` G ) ` x ) = d <-> ( ( od ` G ) ` z ) = d ) )
80 75 76 77 78 79 cbvrabw 
 |-  { x e. B | ( ( od ` G ) ` x ) = d } = { z e. B | ( ( od ` G ) ` z ) = d }
81 80 a1i 
 |-  ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> { x e. B | ( ( od ` G ) ` x ) = d } = { z e. B | ( ( od ` G ) ` z ) = d } )
82 81 fveq2d 
 |-  ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( # ` { z e. B | ( ( od ` G ) ` z ) = d } ) )
83 3 ad5antr 
 |-  ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> G e. Grp )
84 4 ad5antr 
 |-  ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> B e. Fin )
85 nfv 
 |-  F/ z ( n .^ x ) = ( 0g ` G )
86 nfv 
 |-  F/ x ( n .^ z ) = ( 0g ` G )
87 oveq2 
 |-  ( x = z -> ( n .^ x ) = ( n .^ z ) )
88 87 eqeq1d 
 |-  ( x = z -> ( ( n .^ x ) = ( 0g ` G ) <-> ( n .^ z ) = ( 0g ` G ) ) )
89 75 76 85 86 88 cbvrabw 
 |-  { x e. B | ( n .^ x ) = ( 0g ` G ) } = { z e. B | ( n .^ z ) = ( 0g ` G ) }
90 89 a1i 
 |-  ( ph -> { x e. B | ( n .^ x ) = ( 0g ` G ) } = { z e. B | ( n .^ z ) = ( 0g ` G ) } )
91 90 fveq2d 
 |-  ( ph -> ( # ` { x e. B | ( n .^ x ) = ( 0g ` G ) } ) = ( # ` { z e. B | ( n .^ z ) = ( 0g ` G ) } ) )
92 91 breq1d 
 |-  ( ph -> ( ( # ` { x e. B | ( n .^ x ) = ( 0g ` G ) } ) <_ n <-> ( # ` { z e. B | ( n .^ z ) = ( 0g ` G ) } ) <_ n ) )
93 92 ralbidv 
 |-  ( ph -> ( A. n e. NN ( # ` { x e. B | ( n .^ x ) = ( 0g ` G ) } ) <_ n <-> A. n e. NN ( # ` { z e. B | ( n .^ z ) = ( 0g ` G ) } ) <_ n ) )
94 93 biimpd 
 |-  ( ph -> ( A. n e. NN ( # ` { x e. B | ( n .^ x ) = ( 0g ` G ) } ) <_ n -> A. n e. NN ( # ` { z e. B | ( n .^ z ) = ( 0g ` G ) } ) <_ n ) )
95 5 94 mpd 
 |-  ( ph -> A. n e. NN ( # ` { z e. B | ( n .^ z ) = ( 0g ` G ) } ) <_ n )
96 95 ad5antr 
 |-  ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> A. n e. NN ( # ` { z e. B | ( n .^ z ) = ( 0g ` G ) } ) <_ n )
97 simp-5r 
 |-  ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> d e. NN )
98 simpllr 
 |-  ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> d || ( # ` B ) )
99 simplr 
 |-  ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> a e. B )
100 simpr 
 |-  ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> ( ( od ` G ) ` a ) = d )
101 nfv 
 |-  F/ x ( ( od ` G ) ` z ) = c
102 nfv 
 |-  F/ z ( ( od ` G ) ` x ) = c
103 fveqeq2 
 |-  ( z = x -> ( ( ( od ` G ) ` z ) = c <-> ( ( od ` G ) ` x ) = c ) )
104 76 75 101 102 103 cbvrabw 
 |-  { z e. B | ( ( od ` G ) ` z ) = c } = { x e. B | ( ( od ` G ) ` x ) = c }
105 eqcom 
 |-  ( { z e. B | ( ( od ` G ) ` z ) = c } = { x e. B | ( ( od ` G ) ` x ) = c } <-> { x e. B | ( ( od ` G ) ` x ) = c } = { z e. B | ( ( od ` G ) ` z ) = c } )
106 104 105 mpbi 
 |-  { x e. B | ( ( od ` G ) ` x ) = c } = { z e. B | ( ( od ` G ) ` z ) = c }
107 106 neeq1i 
 |-  ( { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) <-> { z e. B | ( ( od ` G ) ` z ) = c } =/= (/) )
108 107 anbi2i 
 |-  ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) <-> ( c || ( # ` B ) /\ { z e. B | ( ( od ` G ) ` z ) = c } =/= (/) ) )
109 106 fveq2i 
 |-  ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( # ` { z e. B | ( ( od ` G ) ` z ) = c } )
110 109 eqeq1i 
 |-  ( ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) <-> ( # ` { z e. B | ( ( od ` G ) ` z ) = c } ) = ( phi ` c ) )
111 108 110 imbi12i 
 |-  ( ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) <-> ( ( c || ( # ` B ) /\ { z e. B | ( ( od ` G ) ` z ) = c } =/= (/) ) -> ( # ` { z e. B | ( ( od ` G ) ` z ) = c } ) = ( phi ` c ) ) )
112 111 imbi2i 
 |-  ( ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) <-> ( c < d -> ( ( c || ( # ` B ) /\ { z e. B | ( ( od ` G ) ` z ) = c } =/= (/) ) -> ( # ` { z e. B | ( ( od ` G ) ` z ) = c } ) = ( phi ` c ) ) ) )
113 112 biimpi 
 |-  ( ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) -> ( c < d -> ( ( c || ( # ` B ) /\ { z e. B | ( ( od ` G ) ` z ) = c } =/= (/) ) -> ( # ` { z e. B | ( ( od ` G ) ` z ) = c } ) = ( phi ` c ) ) ) )
114 113 ralimi 
 |-  ( A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) -> A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { z e. B | ( ( od ` G ) ` z ) = c } =/= (/) ) -> ( # ` { z e. B | ( ( od ` G ) ` z ) = c } ) = ( phi ` c ) ) ) )
115 114 adantl 
 |-  ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) -> A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { z e. B | ( ( od ` G ) ` z ) = c } =/= (/) ) -> ( # ` { z e. B | ( ( od ` G ) ` z ) = c } ) = ( phi ` c ) ) ) )
116 115 adantr 
 |-  ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) -> A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { z e. B | ( ( od ` G ) ` z ) = c } =/= (/) ) -> ( # ` { z e. B | ( ( od ` G ) ` z ) = c } ) = ( phi ` c ) ) ) )
117 116 adantr 
 |-  ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) -> A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { z e. B | ( ( od ` G ) ` z ) = c } =/= (/) ) -> ( # ` { z e. B | ( ( od ` G ) ` z ) = c } ) = ( phi ` c ) ) ) )
118 117 adantr 
 |-  ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { z e. B | ( ( od ` G ) ` z ) = c } =/= (/) ) -> ( # ` { z e. B | ( ( od ` G ) ` z ) = c } ) = ( phi ` c ) ) ) )
119 1 2 83 84 96 97 98 99 100 118 unitscyglem2 
 |-  ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> ( # ` { z e. B | ( ( od ` G ) ` z ) = d } ) = ( phi ` d ) )
120 82 119 eqtrd 
 |-  ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) )
121 74 120 syl 
 |-  ( ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ E. x e. B ( ( od ` G ) ` x ) = d ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) )
122 nfv 
 |-  F/ a ( ( od ` G ) ` x ) = d
123 nfv 
 |-  F/ x ( ( od ` G ) ` a ) = d
124 fveqeq2 
 |-  ( x = a -> ( ( ( od ` G ) ` x ) = d <-> ( ( od ` G ) ` a ) = d ) )
125 122 123 124 cbvrexw 
 |-  ( E. x e. B ( ( od ` G ) ` x ) = d <-> E. a e. B ( ( od ` G ) ` a ) = d )
126 125 bilani 
 |-  ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ E. x e. B ( ( od ` G ) ` x ) = d ) -> E. a e. B ( ( od ` G ) ` a ) = d )
127 121 126 r19.29a 
 |-  ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ E. x e. B ( ( od ` G ) ` x ) = d ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) )
128 127 ex 
 |-  ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) -> ( E. x e. B ( ( od ` G ) ` x ) = d -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) ) )
129 128 adantr 
 |-  ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> ( E. x e. B ( ( od ` G ) ` x ) = d -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) ) )
130 68 129 mpd 
 |-  ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) )
131 66 130 syl 
 |-  ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) )
132 131 ex 
 |-  ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) -> ( ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) ) )
133 132 ex 
 |-  ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) -> ( ph -> ( ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) ) ) )
134 133 ex 
 |-  ( d e. NN -> ( A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) -> ( ph -> ( ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) ) ) ) )
135 15 134 indstr 
 |-  ( d e. NN -> ( ph -> ( ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) ) ) )
136 135 com12 
 |-  ( ph -> ( d e. NN -> ( ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) ) ) )
137 136 imp 
 |-  ( ( ph /\ d e. NN ) -> ( ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) ) )
138 137 ralrimiva 
 |-  ( ph -> A. d e. NN ( ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) ) )