Metamath Proof Explorer

Theorem nosupno

Description: The next several theorems deal with a surreal "supremum". This surreal will ultimately be shown to bound A below and bound the restriction of any surreal above. We begin by showing that the given expression actually defines a surreal number. (Contributed by Scott Fenton, 5-Dec-2021)

Ref Expression
Hypothesis nosupno.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 nosupno 
|- ( ( A C_ No /\ A e. V ) -> S e. No )

Proof

Step Hyp Ref Expression
1 nosupno.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 elex 
 |-  ( A e. V -> A e. _V )
3 iftrue 
 |-  ( 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 ) ) ) ) = ( ( iota_ x e. A A. y e. A -. x . } ) )
4 3 adantr 
 |-  ( ( 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 ) ) ) ) = ( ( iota_ x e. A A. y e. A -. x . } ) )
5 simprl 
 |-  ( ( E. x e. A A. y e. A -. x  A C_ No )
6 simpl 
 |-  ( ( E. x e. A A. y e. A -. x  E. x e. A A. y e. A -. x
7 nomaxmo 
 |-  ( A C_ No -> E* x e. A A. y e. A -. x
8 7 ad2antrl 
 |-  ( ( E. x e. A A. y e. A -. x  E* x e. A A. y e. A -. x
9 reu5 
 |-  ( E! x e. A A. y e. A -. x  ( E. x e. A A. y e. A -. x
10 6 8 9 sylanbrc 
 |-  ( ( E. x e. A A. y e. A -. x  E! x e. A A. y e. A -. x
11 riotacl 
 |-  ( E! x e. A A. y e. A -. x  ( iota_ x e. A A. y e. A -. x
12 10 11 syl 
 |-  ( ( E. x e. A A. y e. A -. x  ( iota_ x e. A A. y e. A -. x
13 5 12 sseldd 
 |-  ( ( E. x e. A A. y e. A -. x  ( iota_ x e. A A. y e. A -. x
14 2on 
 |-  2o e. On
15 14 elexi 
 |-  2o e. _V
16 15 prid2 
 |-  2o e. { 1o , 2o }
17 16 noextend 
 |-  ( ( iota_ x e. A A. y e. A -. x  ( ( iota_ x e. A A. y e. A -. x . } ) e. No )
18 13 17 syl 
 |-  ( ( E. x e. A A. y e. A -. x  ( ( iota_ x e. A A. y e. A -. x . } ) e. No )
19 4 18 eqeltrd 
 |-  ( ( 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 ) ) ) ) e. No )
20 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 ) ) ) )
21 20 adantr 
 |-  ( ( -. 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 ) ) ) )
22 funmpt 
 |-  Fun ( 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 ) ) )
23 22 a1i 
 |-  ( ( -. E. x e. A A. y e. A -. x  Fun ( 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 ) ) ) )
24 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
25 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 ) ) )
26 24 25 dmmpti 
 |-  dom ( 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 ) ) ) = { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) }
27 ssel2 
 |-  ( ( A C_ No /\ u e. A ) -> u e. No )
28 nodmon 
 |-  ( u e. No -> dom u e. On )
29 27 28 syl 
 |-  ( ( A C_ No /\ u e. A ) -> dom u e. On )
30 onss 
 |-  ( dom u e. On -> dom u C_ On )
31 29 30 syl 
 |-  ( ( A C_ No /\ u e. A ) -> dom u C_ On )
32 31 sseld 
 |-  ( ( A C_ No /\ u e. A ) -> ( y e. dom u -> y e. On ) )
33 32 adantrd 
 |-  ( ( A C_ No /\ u e. A ) -> ( ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) -> y e. On ) )
34 33 rexlimdva 
 |-  ( A C_ No -> ( E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) -> y e. On ) )
35 34 abssdv 
 |-  ( A C_ No -> { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } C_ On )
36 simplr 
 |-  ( ( ( A C_ No /\ a e. b ) /\ u e. A ) -> a e. b )
37 29 adantlr 
 |-  ( ( ( A C_ No /\ a e. b ) /\ u e. A ) -> dom u e. On )
38 ontr1 
 |-  ( dom u e. On -> ( ( a e. b /\ b e. dom u ) -> a e. dom u ) )
39 37 38 syl 
 |-  ( ( ( A C_ No /\ a e. b ) /\ u e. A ) -> ( ( a e. b /\ b e. dom u ) -> a e. dom u ) )
40 36 39 mpand 
 |-  ( ( ( A C_ No /\ a e. b ) /\ u e. A ) -> ( b e. dom u -> a e. dom u ) )
41 40 adantrd 
 |-  ( ( ( A C_ No /\ a e. b ) /\ u e. A ) -> ( ( b e. dom u /\ A. v e. A ( -. v  ( u |` suc b ) = ( v |` suc b ) ) ) -> a e. dom u ) )
42 reseq1 
 |-  ( ( u |` suc b ) = ( v |` suc b ) -> ( ( u |` suc b ) |` suc a ) = ( ( v |` suc b ) |` suc a ) )
43 onelon 
 |-  ( ( dom u e. On /\ b e. dom u ) -> b e. On )
44 37 43 sylan 
 |-  ( ( ( ( A C_ No /\ a e. b ) /\ u e. A ) /\ b e. dom u ) -> b e. On )
45 suceloni 
 |-  ( b e. On -> suc b e. On )
46 44 45 syl 
 |-  ( ( ( ( A C_ No /\ a e. b ) /\ u e. A ) /\ b e. dom u ) -> suc b e. On )
47 simpllr 
 |-  ( ( ( ( A C_ No /\ a e. b ) /\ u e. A ) /\ b e. dom u ) -> a e. b )
48 eloni 
 |-  ( b e. On -> Ord b )
49 44 48 syl 
 |-  ( ( ( ( A C_ No /\ a e. b ) /\ u e. A ) /\ b e. dom u ) -> Ord b )
50 ordsucelsuc 
 |-  ( Ord b -> ( a e. b <-> suc a e. suc b ) )
51 49 50 syl 
 |-  ( ( ( ( A C_ No /\ a e. b ) /\ u e. A ) /\ b e. dom u ) -> ( a e. b <-> suc a e. suc b ) )
52 47 51 mpbid 
 |-  ( ( ( ( A C_ No /\ a e. b ) /\ u e. A ) /\ b e. dom u ) -> suc a e. suc b )
53 onelss 
 |-  ( suc b e. On -> ( suc a e. suc b -> suc a C_ suc b ) )
54 46 52 53 sylc 
 |-  ( ( ( ( A C_ No /\ a e. b ) /\ u e. A ) /\ b e. dom u ) -> suc a C_ suc b )
55 54 resabs1d 
 |-  ( ( ( ( A C_ No /\ a e. b ) /\ u e. A ) /\ b e. dom u ) -> ( ( u |` suc b ) |` suc a ) = ( u |` suc a ) )
56 54 resabs1d 
 |-  ( ( ( ( A C_ No /\ a e. b ) /\ u e. A ) /\ b e. dom u ) -> ( ( v |` suc b ) |` suc a ) = ( v |` suc a ) )
57 55 56 eqeq12d 
 |-  ( ( ( ( A C_ No /\ a e. b ) /\ u e. A ) /\ b e. dom u ) -> ( ( ( u |` suc b ) |` suc a ) = ( ( v |` suc b ) |` suc a ) <-> ( u |` suc a ) = ( v |` suc a ) ) )
58 42 57 syl5ib 
 |-  ( ( ( ( A C_ No /\ a e. b ) /\ u e. A ) /\ b e. dom u ) -> ( ( u |` suc b ) = ( v |` suc b ) -> ( u |` suc a ) = ( v |` suc a ) ) )
59 58 imim2d 
 |-  ( ( ( ( A C_ No /\ a e. b ) /\ u e. A ) /\ b e. dom u ) -> ( ( -. v  ( u |` suc b ) = ( v |` suc b ) ) -> ( -. v  ( u |` suc a ) = ( v |` suc a ) ) ) )
60 59 ralimdv 
 |-  ( ( ( ( A C_ No /\ a e. b ) /\ u e. A ) /\ b e. dom u ) -> ( A. v e. A ( -. v  ( u |` suc b ) = ( v |` suc b ) ) -> A. v e. A ( -. v  ( u |` suc a ) = ( v |` suc a ) ) ) )
61 60 expimpd 
 |-  ( ( ( A C_ No /\ a e. b ) /\ u e. A ) -> ( ( b e. dom u /\ A. v e. A ( -. v  ( u |` suc b ) = ( v |` suc b ) ) ) -> A. v e. A ( -. v  ( u |` suc a ) = ( v |` suc a ) ) ) )
62 41 61 jcad 
 |-  ( ( ( A C_ No /\ a e. b ) /\ u e. A ) -> ( ( b e. dom u /\ A. v e. A ( -. v  ( u |` suc b ) = ( v |` suc b ) ) ) -> ( a e. dom u /\ A. v e. A ( -. v  ( u |` suc a ) = ( v |` suc a ) ) ) ) )
63 62 reximdva 
 |-  ( ( A C_ No /\ a e. b ) -> ( E. u e. A ( b e. dom u /\ A. v e. A ( -. v  ( u |` suc b ) = ( v |` suc b ) ) ) -> E. u e. A ( a e. dom u /\ A. v e. A ( -. v  ( u |` suc a ) = ( v |` suc a ) ) ) ) )
64 63 expimpd 
 |-  ( A C_ No -> ( ( a e. b /\ E. u e. A ( b e. dom u /\ A. v e. A ( -. v  ( u |` suc b ) = ( v |` suc b ) ) ) ) -> E. u e. A ( a e. dom u /\ A. v e. A ( -. v  ( u |` suc a ) = ( v |` suc a ) ) ) ) )
65 vex 
 |-  b e. _V
66 eleq1w 
 |-  ( y = b -> ( y e. dom u <-> b e. dom u ) )
67 suceq 
 |-  ( y = b -> suc y = suc b )
68 67 reseq2d 
 |-  ( y = b -> ( u |` suc y ) = ( u |` suc b ) )
69 67 reseq2d 
 |-  ( y = b -> ( v |` suc y ) = ( v |` suc b ) )
70 68 69 eqeq12d 
 |-  ( y = b -> ( ( u |` suc y ) = ( v |` suc y ) <-> ( u |` suc b ) = ( v |` suc b ) ) )
71 70 imbi2d 
 |-  ( y = b -> ( ( -. v  ( u |` suc y ) = ( v |` suc y ) ) <-> ( -. v  ( u |` suc b ) = ( v |` suc b ) ) ) )
72 71 ralbidv 
 |-  ( y = b -> ( A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) <-> A. v e. A ( -. v  ( u |` suc b ) = ( v |` suc b ) ) ) )
73 66 72 anbi12d 
 |-  ( y = b -> ( ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) <-> ( b e. dom u /\ A. v e. A ( -. v  ( u |` suc b ) = ( v |` suc b ) ) ) ) )
74 73 rexbidv 
 |-  ( y = b -> ( E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) <-> E. u e. A ( b e. dom u /\ A. v e. A ( -. v  ( u |` suc b ) = ( v |` suc b ) ) ) ) )
75 65 74 elab 
 |-  ( b e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } <-> E. u e. A ( b e. dom u /\ A. v e. A ( -. v  ( u |` suc b ) = ( v |` suc b ) ) ) )
76 75 anbi2i 
 |-  ( ( a e. b /\ b e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } ) <-> ( a e. b /\ E. u e. A ( b e. dom u /\ A. v e. A ( -. v  ( u |` suc b ) = ( v |` suc b ) ) ) ) )
77 vex 
 |-  a e. _V
78 eleq1w 
 |-  ( y = a -> ( y e. dom u <-> a e. dom u ) )
79 suceq 
 |-  ( y = a -> suc y = suc a )
80 79 reseq2d 
 |-  ( y = a -> ( u |` suc y ) = ( u |` suc a ) )
81 79 reseq2d 
 |-  ( y = a -> ( v |` suc y ) = ( v |` suc a ) )
82 80 81 eqeq12d 
 |-  ( y = a -> ( ( u |` suc y ) = ( v |` suc y ) <-> ( u |` suc a ) = ( v |` suc a ) ) )
83 82 imbi2d 
 |-  ( y = a -> ( ( -. v  ( u |` suc y ) = ( v |` suc y ) ) <-> ( -. v  ( u |` suc a ) = ( v |` suc a ) ) ) )
84 83 ralbidv 
 |-  ( y = a -> ( A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) <-> A. v e. A ( -. v  ( u |` suc a ) = ( v |` suc a ) ) ) )
85 78 84 anbi12d 
 |-  ( y = a -> ( ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) <-> ( a e. dom u /\ A. v e. A ( -. v  ( u |` suc a ) = ( v |` suc a ) ) ) ) )
86 85 rexbidv 
 |-  ( y = a -> ( E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) <-> E. u e. A ( a e. dom u /\ A. v e. A ( -. v  ( u |` suc a ) = ( v |` suc a ) ) ) ) )
87 77 86 elab 
 |-  ( a e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } <-> E. u e. A ( a e. dom u /\ A. v e. A ( -. v  ( u |` suc a ) = ( v |` suc a ) ) ) )
88 64 76 87 3imtr4g 
 |-  ( A C_ No -> ( ( a e. b /\ b e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } ) -> a e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } ) )
89 88 alrimivv 
 |-  ( A C_ No -> A. a A. b ( ( a e. b /\ b e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } ) -> a e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } ) )
90 dftr2 
 |-  ( Tr { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } <-> A. a A. b ( ( a e. b /\ b e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } ) -> a e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } ) )
91 89 90 sylibr 
 |-  ( A C_ No -> Tr { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } )
92 dford5 
 |-  ( Ord { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } <-> ( { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } C_ On /\ Tr { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } ) )
93 35 91 92 sylanbrc 
 |-  ( A C_ No -> Ord { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } )
94 93 adantr 
 |-  ( ( A C_ No /\ A e. _V ) -> Ord { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } )
95 bdayfo 
 |-  bday : No -onto-> On
96 fofun 
 |-  ( bday : No -onto-> On -> Fun bday )
97 95 96 ax-mp 
 |-  Fun bday
98 funimaexg 
 |-  ( ( Fun bday /\ A e. _V ) -> ( bday " A ) e. _V )
99 97 98 mpan 
 |-  ( A e. _V -> ( bday " A ) e. _V )
100 99 uniexd 
 |-  ( A e. _V -> U. ( bday " A ) e. _V )
101 100 adantl 
 |-  ( ( A C_ No /\ A e. _V ) -> U. ( bday " A ) e. _V )
102 simpl 
 |-  ( ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) -> y e. dom u )
103 102 reximi 
 |-  ( E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) -> E. u e. A y e. dom u )
104 103 ss2abi 
 |-  { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } C_ { y | E. u e. A y e. dom u }
105 bdayval 
 |-  ( u e. No -> ( bday ` u ) = dom u )
106 27 105 syl 
 |-  ( ( A C_ No /\ u e. A ) -> ( bday ` u ) = dom u )
107 fofn 
 |-  ( bday : No -onto-> On -> bday Fn No )
108 95 107 ax-mp 
 |-  bday Fn No
109 fnfvima 
 |-  ( ( bday Fn No /\ A C_ No /\ u e. A ) -> ( bday ` u ) e. ( bday " A ) )
110 108 109 mp3an1 
 |-  ( ( A C_ No /\ u e. A ) -> ( bday ` u ) e. ( bday " A ) )
111 106 110 eqeltrrd 
 |-  ( ( A C_ No /\ u e. A ) -> dom u e. ( bday " A ) )
112 elssuni 
 |-  ( dom u e. ( bday " A ) -> dom u C_ U. ( bday " A ) )
113 111 112 syl 
 |-  ( ( A C_ No /\ u e. A ) -> dom u C_ U. ( bday " A ) )
114 113 sseld 
 |-  ( ( A C_ No /\ u e. A ) -> ( y e. dom u -> y e. U. ( bday " A ) ) )
115 114 rexlimdva 
 |-  ( A C_ No -> ( E. u e. A y e. dom u -> y e. U. ( bday " A ) ) )
116 115 abssdv 
 |-  ( A C_ No -> { y | E. u e. A y e. dom u } C_ U. ( bday " A ) )
117 116 adantr 
 |-  ( ( A C_ No /\ A e. _V ) -> { y | E. u e. A y e. dom u } C_ U. ( bday " A ) )
118 104 117 sstrid 
 |-  ( ( A C_ No /\ A e. _V ) -> { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } C_ U. ( bday " A ) )
119 101 118 ssexd 
 |-  ( ( A C_ No /\ A e. _V ) -> { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } e. _V )
120 elong 
 |-  ( { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } e. _V -> ( { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } e. On <-> Ord { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } ) )
121 119 120 syl 
 |-  ( ( A C_ No /\ A e. _V ) -> ( { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } e. On <-> Ord { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } ) )
122 94 121 mpbird 
 |-  ( ( A C_ No /\ A e. _V ) -> { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } e. On )
123 26 122 eqeltrid 
 |-  ( ( A C_ No /\ A e. _V ) -> dom ( 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 ) ) ) e. On )
124 123 adantl 
 |-  ( ( -. E. x e. A A. y e. A -. x  dom ( 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 ) ) ) e. On )
125 25 rnmpt 
 |-  ran ( 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 ) ) ) = { z | E. g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } z = ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) }
126 vex 
 |-  g e. _V
127 eleq1w 
 |-  ( y = g -> ( y e. dom u <-> g e. dom u ) )
128 suceq 
 |-  ( y = g -> suc y = suc g )
129 128 reseq2d 
 |-  ( y = g -> ( u |` suc y ) = ( u |` suc g ) )
130 128 reseq2d 
 |-  ( y = g -> ( v |` suc y ) = ( v |` suc g ) )
131 129 130 eqeq12d 
 |-  ( y = g -> ( ( u |` suc y ) = ( v |` suc y ) <-> ( u |` suc g ) = ( v |` suc g ) ) )
132 131 imbi2d 
 |-  ( y = g -> ( ( -. v  ( u |` suc y ) = ( v |` suc y ) ) <-> ( -. v  ( u |` suc g ) = ( v |` suc g ) ) ) )
133 132 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 ) ) ) )
134 127 133 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 ) ) ) ) )
135 134 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 ) ) ) ) )
136 126 135 elab 
 |-  ( g e. { y | 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 ) ) ) )
137 eqid 
 |-  ( u ` g ) = ( u ` g )
138 fvex 
 |-  ( u ` g ) e. _V
139 eqeq2 
 |-  ( x = ( u ` g ) -> ( ( u ` g ) = x <-> ( u ` g ) = ( u ` g ) ) )
140 139 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 ) ) ) )
141 138 140 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 ) )
142 137 141 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 ) )
143 142 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 ) )
144 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 ) )
145 143 144 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 ) )
146 145 adantl 
 |-  ( ( A C_ No /\ 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 ) )
147 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 ) )
148 147 adantr 
 |-  ( ( A C_ No /\ 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 ) )
149 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 ) ) )
150 146 148 149 sylanbrc 
 |-  ( ( A C_ No /\ 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 ) )
151 vex 
 |-  z e. _V
152 eqeq2 
 |-  ( x = z -> ( ( u ` g ) = x <-> ( u ` g ) = z ) )
153 152 3anbi3d 
 |-  ( x = z -> ( ( 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 ) = z ) ) )
154 153 rexbidv 
 |-  ( x = z -> ( 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 ) = z ) ) )
155 154 iota2 
 |-  ( ( z 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 ) = z ) <-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) = z ) )
156 151 155 mpan 
 |-  ( 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 ) = z ) <-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) = z ) )
157 150 156 syl 
 |-  ( ( A C_ No /\ E. 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 ) = z ) <-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) = z ) )
158 eqcom 
 |-  ( ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) = z <-> z = ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) )
159 157 158 bitrdi 
 |-  ( ( A C_ No /\ E. 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 ) = z ) <-> z = ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
160 simprr3 
 |-  ( ( A C_ No /\ ( u e. A /\ ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = z ) ) ) -> ( u ` g ) = z )
161 27 adantrr 
 |-  ( ( A C_ No /\ ( u e. A /\ ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = z ) ) ) -> u e. No )
162 norn 
 |-  ( u e. No -> ran u C_ { 1o , 2o } )
163 161 162 syl 
 |-  ( ( A C_ No /\ ( u e. A /\ ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = z ) ) ) -> ran u C_ { 1o , 2o } )
164 nofun 
 |-  ( u e. No -> Fun u )
165 161 164 syl 
 |-  ( ( A C_ No /\ ( u e. A /\ ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = z ) ) ) -> Fun u )
166 simprr1 
 |-  ( ( A C_ No /\ ( u e. A /\ ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = z ) ) ) -> g e. dom u )
167 fvelrn 
 |-  ( ( Fun u /\ g e. dom u ) -> ( u ` g ) e. ran u )
168 165 166 167 syl2anc 
 |-  ( ( A C_ No /\ ( u e. A /\ ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = z ) ) ) -> ( u ` g ) e. ran u )
169 163 168 sseldd 
 |-  ( ( A C_ No /\ ( u e. A /\ ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = z ) ) ) -> ( u ` g ) e. { 1o , 2o } )
170 160 169 eqeltrrd 
 |-  ( ( A C_ No /\ ( u e. A /\ ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = z ) ) ) -> z e. { 1o , 2o } )
171 170 rexlimdvaa 
 |-  ( A C_ No -> ( E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = z ) -> z e. { 1o , 2o } ) )
172 171 adantr 
 |-  ( ( A C_ No /\ E. 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 ) = z ) -> z e. { 1o , 2o } ) )
173 159 172 sylbird 
 |-  ( ( A C_ No /\ E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) ) ) -> ( z = ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) -> z e. { 1o , 2o } ) )
174 136 173 sylan2b 
 |-  ( ( A C_ No /\ g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } ) -> ( z = ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) -> z e. { 1o , 2o } ) )
175 174 rexlimdva 
 |-  ( A C_ No -> ( E. g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } z = ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) -> z e. { 1o , 2o } ) )
176 175 abssdv 
 |-  ( A C_ No -> { z | E. g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } z = ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) } C_ { 1o , 2o } )
177 125 176 eqsstrid 
 |-  ( A C_ No -> ran ( 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 ) ) ) C_ { 1o , 2o } )
178 177 ad2antrl 
 |-  ( ( -. E. x e. A A. y e. A -. x  ran ( 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 ) ) ) C_ { 1o , 2o } )
179 elno2 
 |-  ( ( 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 ) ) ) e. No <-> ( Fun ( 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 ) ) ) /\ dom ( 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 ) ) ) e. On /\ ran ( 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 ) ) ) C_ { 1o , 2o } ) )
180 23 124 178 179 syl3anbrc 
 |-  ( ( -. 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 ) ) ) e. No )
181 21 180 eqeltrd 
 |-  ( ( -. 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 ) ) ) ) e. No )
182 19 181 pm2.61ian 
 |-  ( ( A C_ No /\ A e. _V ) -> 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 ) ) ) ) e. No )
183 1 182 eqeltrid 
 |-  ( ( A C_ No /\ A e. _V ) -> S e. No )
184 2 183 sylan2 
 |-  ( ( A C_ No /\ A e. V ) -> S e. No )