Metamath Proof Explorer

Theorem nosupfv

Description: The value of surreal supremum when there is no maximum. (Contributed by Scott Fenton, 5-Dec-2021)

Ref Expression
Hypothesis nosupfv.1 
|- S = if ( E. x e. A A. y e. A -. x . } ) , ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
Assertion nosupfv 
|- ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( S ` G ) = ( U ` G ) )

Proof

Step Hyp Ref Expression
1 nosupfv.1 
 |-  S = if ( E. x e. A A. y e. A -. x . } ) , ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
2 iffalse 
 |-  ( -. E. x e. A A. y e. A -. x  if ( E. x e. A A. y e. A -. x . } ) , ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) ) = ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
3 1 2 syl5eq 
 |-  ( -. E. x e. A A. y e. A -. x  S = ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
4 3 fveq1d 
 |-  ( -. E. x e. A A. y e. A -. x  ( S ` G ) = ( ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) ` G ) )
5 4 3ad2ant1 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( S ` G ) = ( ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) ` G ) )
6 simp32 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> G e. dom U )
7 dmeq 
 |-  ( p = U -> dom p = dom U )
8 7 eleq2d 
 |-  ( p = U -> ( G e. dom p <-> G e. dom U ) )
9 breq2 
 |-  ( p = U -> ( v  v
10 9 notbid 
 |-  ( p = U -> ( -. v  -. v
11 reseq1 
 |-  ( p = U -> ( p |` suc G ) = ( U |` suc G ) )
12 11 eqeq1d 
 |-  ( p = U -> ( ( p |` suc G ) = ( v |` suc G ) <-> ( U |` suc G ) = ( v |` suc G ) ) )
13 10 12 imbi12d 
 |-  ( p = U -> ( ( -. v  ( p |` suc G ) = ( v |` suc G ) ) <-> ( -. v  ( U |` suc G ) = ( v |` suc G ) ) ) )
14 13 ralbidv 
 |-  ( p = U -> ( A. v e. A ( -. v  ( p |` suc G ) = ( v |` suc G ) ) <-> A. v e. A ( -. v  ( U |` suc G ) = ( v |` suc G ) ) ) )
15 8 14 anbi12d 
 |-  ( p = U -> ( ( G e. dom p /\ A. v e. A ( -. v  ( p |` suc G ) = ( v |` suc G ) ) ) <-> ( G e. dom U /\ A. v e. A ( -. v  ( U |` suc G ) = ( v |` suc G ) ) ) ) )
16 15 rspcev 
 |-  ( ( U e. A /\ ( G e. dom U /\ A. v e. A ( -. v  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> E. p e. A ( G e. dom p /\ A. v e. A ( -. v  ( p |` suc G ) = ( v |` suc G ) ) ) )
17 16 3impb 
 |-  ( ( U e. A /\ G e. dom U /\ A. v e. A ( -. v  ( U |` suc G ) = ( v |` suc G ) ) ) -> E. p e. A ( G e. dom p /\ A. v e. A ( -. v  ( p |` suc G ) = ( v |` suc G ) ) ) )
18 dmeq 
 |-  ( u = p -> dom u = dom p )
19 18 eleq2d 
 |-  ( u = p -> ( G e. dom u <-> G e. dom p ) )
20 breq2 
 |-  ( u = p -> ( v  v
21 20 notbid 
 |-  ( u = p -> ( -. v  -. v
22 reseq1 
 |-  ( u = p -> ( u |` suc G ) = ( p |` suc G ) )
23 22 eqeq1d 
 |-  ( u = p -> ( ( u |` suc G ) = ( v |` suc G ) <-> ( p |` suc G ) = ( v |` suc G ) ) )
24 21 23 imbi12d 
 |-  ( u = p -> ( ( -. v  ( u |` suc G ) = ( v |` suc G ) ) <-> ( -. v  ( p |` suc G ) = ( v |` suc G ) ) ) )
25 24 ralbidv 
 |-  ( u = p -> ( A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) <-> A. v e. A ( -. v  ( p |` suc G ) = ( v |` suc G ) ) ) )
26 19 25 anbi12d 
 |-  ( u = p -> ( ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) ) <-> ( G e. dom p /\ A. v e. A ( -. v  ( p |` suc G ) = ( v |` suc G ) ) ) ) )
27 26 cbvrexvw 
 |-  ( E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) ) <-> E. p e. A ( G e. dom p /\ A. v e. A ( -. v  ( p |` suc G ) = ( v |` suc G ) ) ) )
28 17 27 sylibr 
 |-  ( ( U e. A /\ G e. dom U /\ A. v e. A ( -. v  ( U |` suc G ) = ( v |` suc G ) ) ) -> E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) ) )
29 28 3ad2ant3 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) ) )
30 eleq1 
 |-  ( y = G -> ( y e. dom u <-> G e. dom u ) )
31 suceq 
 |-  ( y = G -> suc y = suc G )
32 31 reseq2d 
 |-  ( y = G -> ( u |` suc y ) = ( u |` suc G ) )
33 31 reseq2d 
 |-  ( y = G -> ( v |` suc y ) = ( v |` suc G ) )
34 32 33 eqeq12d 
 |-  ( y = G -> ( ( u |` suc y ) = ( v |` suc y ) <-> ( u |` suc G ) = ( v |` suc G ) ) )
35 34 imbi2d 
 |-  ( y = G -> ( ( -. v  ( u |` suc y ) = ( v |` suc y ) ) <-> ( -. v  ( u |` suc G ) = ( v |` suc G ) ) ) )
36 35 ralbidv 
 |-  ( y = G -> ( A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) <-> A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) ) )
37 30 36 anbi12d 
 |-  ( y = G -> ( ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) <-> ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) ) ) )
38 37 rexbidv 
 |-  ( y = G -> ( E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) <-> E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) ) ) )
39 6 29 38 elabd 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> G e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } )
40 eleq1 
 |-  ( g = G -> ( g e. dom u <-> G e. dom u ) )
41 suceq 
 |-  ( g = G -> suc g = suc G )
42 41 reseq2d 
 |-  ( g = G -> ( u |` suc g ) = ( u |` suc G ) )
43 41 reseq2d 
 |-  ( g = G -> ( v |` suc g ) = ( v |` suc G ) )
44 42 43 eqeq12d 
 |-  ( g = G -> ( ( u |` suc g ) = ( v |` suc g ) <-> ( u |` suc G ) = ( v |` suc G ) ) )
45 44 imbi2d 
 |-  ( g = G -> ( ( -. v  ( u |` suc g ) = ( v |` suc g ) ) <-> ( -. v  ( u |` suc G ) = ( v |` suc G ) ) ) )
46 45 ralbidv 
 |-  ( g = G -> ( A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) <-> A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) ) )
47 fveqeq2 
 |-  ( g = G -> ( ( u ` g ) = x <-> ( u ` G ) = x ) )
48 40 46 47 3anbi123d 
 |-  ( g = G -> ( ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) <-> ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) ) )
49 48 rexbidv 
 |-  ( g = G -> ( E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) <-> E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) ) )
50 49 iotabidv 
 |-  ( g = G -> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) = ( iota x E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) ) )
51 eqid 
 |-  ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) = ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) )
52 iotaex 
 |-  ( iota x E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) ) e. _V
53 50 51 52 fvmpt 
 |-  ( G e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } -> ( ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) ` G ) = ( iota x E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) ) )
54 39 53 syl 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) ` G ) = ( iota x E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) ) )
55 simp1 
 |-  ( ( U e. A /\ G e. dom U /\ A. v e. A ( -. v  ( U |` suc G ) = ( v |` suc G ) ) ) -> U e. A )
56 simp2 
 |-  ( ( U e. A /\ G e. dom U /\ A. v e. A ( -. v  ( U |` suc G ) = ( v |` suc G ) ) ) -> G e. dom U )
57 simp3 
 |-  ( ( U e. A /\ G e. dom U /\ A. v e. A ( -. v  ( U |` suc G ) = ( v |` suc G ) ) ) -> A. v e. A ( -. v  ( U |` suc G ) = ( v |` suc G ) ) )
58 eqidd 
 |-  ( ( U e. A /\ G e. dom U /\ A. v e. A ( -. v  ( U |` suc G ) = ( v |` suc G ) ) ) -> ( U ` G ) = ( U ` G ) )
59 dmeq 
 |-  ( u = U -> dom u = dom U )
60 59 eleq2d 
 |-  ( u = U -> ( G e. dom u <-> G e. dom U ) )
61 breq2 
 |-  ( u = U -> ( v  v
62 61 notbid 
 |-  ( u = U -> ( -. v  -. v
63 reseq1 
 |-  ( u = U -> ( u |` suc G ) = ( U |` suc G ) )
64 63 eqeq1d 
 |-  ( u = U -> ( ( u |` suc G ) = ( v |` suc G ) <-> ( U |` suc G ) = ( v |` suc G ) ) )
65 62 64 imbi12d 
 |-  ( u = U -> ( ( -. v  ( u |` suc G ) = ( v |` suc G ) ) <-> ( -. v  ( U |` suc G ) = ( v |` suc G ) ) ) )
66 65 ralbidv 
 |-  ( u = U -> ( A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) <-> A. v e. A ( -. v  ( U |` suc G ) = ( v |` suc G ) ) ) )
67 fveq1 
 |-  ( u = U -> ( u ` G ) = ( U ` G ) )
68 67 eqeq1d 
 |-  ( u = U -> ( ( u ` G ) = ( U ` G ) <-> ( U ` G ) = ( U ` G ) ) )
69 60 66 68 3anbi123d 
 |-  ( u = U -> ( ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = ( U ` G ) ) <-> ( G e. dom U /\ A. v e. A ( -. v  ( U |` suc G ) = ( v |` suc G ) ) /\ ( U ` G ) = ( U ` G ) ) ) )
70 69 rspcev 
 |-  ( ( U e. A /\ ( G e. dom U /\ A. v e. A ( -. v  ( U |` suc G ) = ( v |` suc G ) ) /\ ( U ` G ) = ( U ` G ) ) ) -> E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = ( U ` G ) ) )
71 55 56 57 58 70 syl13anc 
 |-  ( ( U e. A /\ G e. dom U /\ A. v e. A ( -. v  ( U |` suc G ) = ( v |` suc G ) ) ) -> E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = ( U ` G ) ) )
72 71 3ad2ant3 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = ( U ` G ) ) )
73 fvex 
 |-  ( U ` G ) e. _V
74 eqid 
 |-  ( u ` G ) = ( u ` G )
75 fvex 
 |-  ( u ` G ) e. _V
76 eqeq2 
 |-  ( x = ( u ` G ) -> ( ( u ` G ) = x <-> ( u ` G ) = ( u ` G ) ) )
77 76 3anbi3d 
 |-  ( x = ( u ` G ) -> ( ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) <-> ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = ( u ` G ) ) ) )
78 75 77 spcev 
 |-  ( ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = ( u ` G ) ) -> E. x ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) )
79 74 78 mp3an3 
 |-  ( ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) ) -> E. x ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) )
80 79 reximi 
 |-  ( E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) ) -> E. u e. A E. x ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) )
81 rexcom4 
 |-  ( E. u e. A E. x ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) <-> E. x E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) )
82 80 81 sylib 
 |-  ( E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) ) -> E. x E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) )
83 28 82 syl 
 |-  ( ( U e. A /\ G e. dom U /\ A. v e. A ( -. v  ( U |` suc G ) = ( v |` suc G ) ) ) -> E. x E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) )
84 83 3ad2ant3 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> E. x E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) )
85 nosupprefixmo 
 |-  ( A C_ No -> E* x E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) )
86 85 adantr 
 |-  ( ( A C_ No /\ A e. _V ) -> E* x E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) )
87 86 3ad2ant2 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> E* x E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) )
88 df-eu 
 |-  ( E! x E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) <-> ( E. x E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ E* x E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) ) )
89 84 87 88 sylanbrc 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> E! x E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) )
90 eqeq2 
 |-  ( x = ( U ` G ) -> ( ( u ` G ) = x <-> ( u ` G ) = ( U ` G ) ) )
91 90 3anbi3d 
 |-  ( x = ( U ` G ) -> ( ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) <-> ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = ( U ` G ) ) ) )
92 91 rexbidv 
 |-  ( x = ( U ` G ) -> ( E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) <-> E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = ( U ` G ) ) ) )
93 92 iota2 
 |-  ( ( ( U ` G ) e. _V /\ E! x E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) ) -> ( E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = ( U ` G ) ) <-> ( iota x E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) ) = ( U ` G ) ) )
94 73 89 93 sylancr 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = ( U ` G ) ) <-> ( iota x E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) ) = ( U ` G ) ) )
95 72 94 mpbid 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( iota x E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) ) = ( U ` G ) )
96 5 54 95 3eqtrd 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( S ` G ) = ( U ` G ) )