Metamath Proof Explorer

Theorem noinfno

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

Ref Expression
Hypothesis noinfno.1 
|- T = if ( E. x e. B A. y e. B -. y . } ) , ( g e. { y | E. u e. B ( y e. dom u /\ A. v e. B ( -. u  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. B ( g e. dom u /\ A. v e. B ( -. u  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
Assertion noinfno 
|- ( ( B C_ No /\ B e. V ) -> T e. No )

Proof

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