Metamath Proof Explorer

Theorem noetainflem4

Description: Lemma for noeta . If A precedes B , then W is greater than A . (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypotheses noetainflem.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 ) ) ) )
noetainflem.2 
|- W = ( T u. ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) )
Assertion noetainflem4 
|- ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  A. a e. A a

Proof

Step Hyp Ref Expression
1 noetainflem.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 noetainflem.2 
 |-  W = ( T u. ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) )
3 simplrl 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ a e. A ) -> B C_ No )
4 simplrr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ a e. A ) -> B e. _V )
5 simpll 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) -> A C_ No )
6 5 sselda 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ a e. A ) -> a e. No )
7 1 noinfbnd2 
 |-  ( ( B C_ No /\ B e. _V /\ a e. No ) -> ( A. b e. B a  -. T
8 3 4 6 7 syl3anc 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ a e. A ) -> ( A. b e. B a  -. T
9 simplll 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  A C_ No )
10 simprl 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  a e. A )
11 9 10 sseldd 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  a e. No )
12 nodmord 
 |-  ( a e. No -> Ord dom a )
13 ordirr 
 |-  ( Ord dom a -> -. dom a e. dom a )
14 11 12 13 3syl 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  -. dom a e. dom a )
15 bdayval 
 |-  ( a e. No -> ( bday ` a ) = dom a )
16 11 15 syl 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( bday ` a ) = dom a )
17 bdayfo 
 |-  bday : No -onto-> On
18 fofn 
 |-  ( bday : No -onto-> On -> bday Fn No )
19 17 18 ax-mp 
 |-  bday Fn No
20 fnfvima 
 |-  ( ( bday Fn No /\ A C_ No /\ a e. A ) -> ( bday ` a ) e. ( bday " A ) )
21 19 9 10 20 mp3an2i 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( bday ` a ) e. ( bday " A ) )
22 16 21 eqeltrrd 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  dom a e. ( bday " A ) )
23 elssuni 
 |-  ( dom a e. ( bday " A ) -> dom a C_ U. ( bday " A ) )
24 22 23 syl 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  dom a C_ U. ( bday " A ) )
25 nodmon 
 |-  ( a e. No -> dom a e. On )
26 imassrn 
 |-  ( bday " A ) C_ ran bday
27 forn 
 |-  ( bday : No -onto-> On -> ran bday = On )
28 17 27 ax-mp 
 |-  ran bday = On
29 26 28 sseqtri 
 |-  ( bday " A ) C_ On
30 ssorduni 
 |-  ( ( bday " A ) C_ On -> Ord U. ( bday " A ) )
31 29 30 ax-mp 
 |-  Ord U. ( bday " A )
32 ordsssuc 
 |-  ( ( dom a e. On /\ Ord U. ( bday " A ) ) -> ( dom a C_ U. ( bday " A ) <-> dom a e. suc U. ( bday " A ) ) )
33 31 32 mpan2 
 |-  ( dom a e. On -> ( dom a C_ U. ( bday " A ) <-> dom a e. suc U. ( bday " A ) ) )
34 11 25 33 3syl 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( dom a C_ U. ( bday " A ) <-> dom a e. suc U. ( bday " A ) ) )
35 24 34 mpbid 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  dom a e. suc U. ( bday " A ) )
36 elun2 
 |-  ( dom a e. suc U. ( bday " A ) -> dom a e. ( dom T u. suc U. ( bday " A ) ) )
37 35 36 syl 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  dom a e. ( dom T u. suc U. ( bday " A ) ) )
38 eleq2 
 |-  ( dom a = ( dom T u. suc U. ( bday " A ) ) -> ( dom a e. dom a <-> dom a e. ( dom T u. suc U. ( bday " A ) ) ) )
39 37 38 syl5ibrcom 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( dom a = ( dom T u. suc U. ( bday " A ) ) -> dom a e. dom a ) )
40 14 39 mtod 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  -. dom a = ( dom T u. suc U. ( bday " A ) ) )
41 dmeq 
 |-  ( a = W -> dom a = dom W )
42 2 dmeqi 
 |-  dom W = dom ( T u. ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) )
43 dmun 
 |-  dom ( T u. ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) ) = ( dom T u. dom ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) )
44 2oex 
 |-  2o e. _V
45 44 snnz 
 |-  { 2o } =/= (/)
46 dmxp 
 |-  ( { 2o } =/= (/) -> dom ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) = ( suc U. ( bday " A ) \ dom T ) )
47 45 46 ax-mp 
 |-  dom ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) = ( suc U. ( bday " A ) \ dom T )
48 47 uneq2i 
 |-  ( dom T u. dom ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) ) = ( dom T u. ( suc U. ( bday " A ) \ dom T ) )
49 undif2 
 |-  ( dom T u. ( suc U. ( bday " A ) \ dom T ) ) = ( dom T u. suc U. ( bday " A ) )
50 48 49 eqtri 
 |-  ( dom T u. dom ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) ) = ( dom T u. suc U. ( bday " A ) )
51 42 43 50 3eqtri 
 |-  dom W = ( dom T u. suc U. ( bday " A ) )
52 41 51 eqtrdi 
 |-  ( a = W -> dom a = ( dom T u. suc U. ( bday " A ) ) )
53 40 52 nsyl 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  -. a = W )
54 53 neqned 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  a =/= W )
55 simpr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  |^| { p e. On | ( a ` p ) =/= ( W ` p ) } e. dom T )
56 11 adantr 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  a e. No )
57 56 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  a e. No )
58 simp-4r 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  A e. _V )
59 simplrl 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  B C_ No )
60 59 adantr 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  B C_ No )
61 simplrr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  B e. _V )
62 61 adantr 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  B e. _V )
63 1 2 noetainflem1 
 |-  ( ( A e. _V /\ B C_ No /\ B e. _V ) -> W e. No )
64 58 60 62 63 syl3anc 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  W e. No )
65 64 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  W e. No )
66 simplr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  a =/= W )
67 nosepne 
 |-  ( ( a e. No /\ W e. No /\ a =/= W ) -> ( a ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) =/= ( W ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) )
68 57 65 66 67 syl3anc 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( a ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) =/= ( W ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) )
69 55 fvresd 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( ( W |` dom T ) ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) = ( W ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) )
70 simp-4r 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( B C_ No /\ B e. _V ) )
71 1 2 noetainflem2 
 |-  ( ( B C_ No /\ B e. _V ) -> ( W |` dom T ) = T )
72 70 71 syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( W |` dom T ) = T )
73 72 fveq1d 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( ( W |` dom T ) ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) = ( T ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) )
74 69 73 eqtr3d 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( W ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) = ( T ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) )
75 68 74 neeqtrd 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( a ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) =/= ( T ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) )
76 75 necomd 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( T ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) =/= ( a ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) )
77 fveq2 
 |-  ( q = |^| { p e. On | ( a ` p ) =/= ( W ` p ) } -> ( T ` q ) = ( T ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) )
78 fveq2 
 |-  ( q = |^| { p e. On | ( a ` p ) =/= ( W ` p ) } -> ( a ` q ) = ( a ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) )
79 77 78 neeq12d 
 |-  ( q = |^| { p e. On | ( a ` p ) =/= ( W ` p ) } -> ( ( T ` q ) =/= ( a ` q ) <-> ( T ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) =/= ( a ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) ) )
80 79 rspcev 
 |-  ( ( |^| { p e. On | ( a ` p ) =/= ( W ` p ) } e. dom T /\ ( T ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) =/= ( a ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) ) -> E. q e. dom T ( T ` q ) =/= ( a ` q ) )
81 55 76 80 syl2anc 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  E. q e. dom T ( T ` q ) =/= ( a ` q ) )
82 df-ne 
 |-  ( ( T ` q ) =/= ( ( a |` dom T ) ` q ) <-> -. ( T ` q ) = ( ( a |` dom T ) ` q ) )
83 fvres 
 |-  ( q e. dom T -> ( ( a |` dom T ) ` q ) = ( a ` q ) )
84 83 neeq2d 
 |-  ( q e. dom T -> ( ( T ` q ) =/= ( ( a |` dom T ) ` q ) <-> ( T ` q ) =/= ( a ` q ) ) )
85 82 84 bitr3id 
 |-  ( q e. dom T -> ( -. ( T ` q ) = ( ( a |` dom T ) ` q ) <-> ( T ` q ) =/= ( a ` q ) ) )
86 85 rexbiia 
 |-  ( E. q e. dom T -. ( T ` q ) = ( ( a |` dom T ) ` q ) <-> E. q e. dom T ( T ` q ) =/= ( a ` q ) )
87 rexnal 
 |-  ( E. q e. dom T -. ( T ` q ) = ( ( a |` dom T ) ` q ) <-> -. A. q e. dom T ( T ` q ) = ( ( a |` dom T ) ` q ) )
88 86 87 bitr3i 
 |-  ( E. q e. dom T ( T ` q ) =/= ( a ` q ) <-> -. A. q e. dom T ( T ` q ) = ( ( a |` dom T ) ` q ) )
89 81 88 sylib 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  -. A. q e. dom T ( T ` q ) = ( ( a |` dom T ) ` q ) )
90 89 olcd 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( -. dom T = dom ( a |` dom T ) \/ -. A. q e. dom T ( T ` q ) = ( ( a |` dom T ) ` q ) ) )
91 1 noinfno 
 |-  ( ( B C_ No /\ B e. _V ) -> T e. No )
92 91 ad3antlr 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  T e. No )
93 92 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  T e. No )
94 nofun 
 |-  ( T e. No -> Fun T )
95 93 94 syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  Fun T )
96 nofun 
 |-  ( a e. No -> Fun a )
97 funres 
 |-  ( Fun a -> Fun ( a |` dom T ) )
98 57 96 97 3syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  Fun ( a |` dom T ) )
99 eqfunfv 
 |-  ( ( Fun T /\ Fun ( a |` dom T ) ) -> ( T = ( a |` dom T ) <-> ( dom T = dom ( a |` dom T ) /\ A. q e. dom T ( T ` q ) = ( ( a |` dom T ) ` q ) ) ) )
100 95 98 99 syl2anc 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( T = ( a |` dom T ) <-> ( dom T = dom ( a |` dom T ) /\ A. q e. dom T ( T ` q ) = ( ( a |` dom T ) ` q ) ) ) )
101 ianor 
 |-  ( -. ( dom T = dom ( a |` dom T ) /\ A. q e. dom T ( T ` q ) = ( ( a |` dom T ) ` q ) ) <-> ( -. dom T = dom ( a |` dom T ) \/ -. A. q e. dom T ( T ` q ) = ( ( a |` dom T ) ` q ) ) )
102 101 con1bii 
 |-  ( -. ( -. dom T = dom ( a |` dom T ) \/ -. A. q e. dom T ( T ` q ) = ( ( a |` dom T ) ` q ) ) <-> ( dom T = dom ( a |` dom T ) /\ A. q e. dom T ( T ` q ) = ( ( a |` dom T ) ` q ) ) )
103 100 102 bitr4di 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( T = ( a |` dom T ) <-> -. ( -. dom T = dom ( a |` dom T ) \/ -. A. q e. dom T ( T ` q ) = ( ( a |` dom T ) ` q ) ) ) )
104 103 con2bid 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( ( -. dom T = dom ( a |` dom T ) \/ -. A. q e. dom T ( T ` q ) = ( ( a |` dom T ) ` q ) ) <-> -. T = ( a |` dom T ) ) )
105 90 104 mpbid 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  -. T = ( a |` dom T ) )
106 105 pm2.21d 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( T = ( a |` dom T ) -> a
107 72 breq2d 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( ( a |` dom T )  ( a |` dom T )
108 nodmon 
 |-  ( T e. No -> dom T e. On )
109 92 108 syl 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  dom T e. On )
110 109 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  dom T e. On )
111 sltres 
 |-  ( ( a e. No /\ W e. No /\ dom T e. On ) -> ( ( a |` dom T )  a
112 57 65 110 111 syl3anc 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( ( a |` dom T )  a
113 107 112 sylbird 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( ( a |` dom T )  a
114 simplrr 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  -. T
115 114 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  -. T
116 noreson 
 |-  ( ( a e. No /\ dom T e. On ) -> ( a |` dom T ) e. No )
117 56 109 116 syl2anc 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( a |` dom T ) e. No )
118 117 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( a |` dom T ) e. No )
119 sltso 
 |-
120 sotric 
 |-  ( (  ( T  -. ( T = ( a |` dom T ) \/ ( a |` dom T )
121 119 120 mpan 
 |-  ( ( T e. No /\ ( a |` dom T ) e. No ) -> ( T  -. ( T = ( a |` dom T ) \/ ( a |` dom T )
122 93 118 121 syl2anc 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( T  -. ( T = ( a |` dom T ) \/ ( a |` dom T )
123 122 con2bid 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( ( T = ( a |` dom T ) \/ ( a |` dom T )  -. T
124 115 123 mpbird 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( T = ( a |` dom T ) \/ ( a |` dom T )
125 106 113 124 mpjaod 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  a
126 64 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  W e. No )
127 56 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  a e. No )
128 simplr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  a =/= W )
129 128 necomd 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  W =/= a )
130 2 fveq1i 
 |-  ( W ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) = ( ( T u. ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) ) ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } )
131 92 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  T e. No )
132 131 94 syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  Fun T )
133 132 funfnd 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  T Fn dom T )
134 fnconstg 
 |-  ( 2o e. _V -> ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) Fn ( suc U. ( bday " A ) \ dom T ) )
135 44 134 ax-mp 
 |-  ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) Fn ( suc U. ( bday " A ) \ dom T )
136 135 a1i 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) Fn ( suc U. ( bday " A ) \ dom T ) )
137 disjdif 
 |-  ( dom T i^i ( suc U. ( bday " A ) \ dom T ) ) = (/)
138 137 a1i 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( dom T i^i ( suc U. ( bday " A ) \ dom T ) ) = (/) )
139 nosepssdm 
 |-  ( ( a e. No /\ W e. No /\ a =/= W ) -> |^| { p e. On | ( a ` p ) =/= ( W ` p ) } C_ dom a )
140 127 126 128 139 syl3anc 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  |^| { p e. On | ( a ` p ) =/= ( W ` p ) } C_ dom a )
141 127 15 syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( bday ` a ) = dom a )
142 simp-5l 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  A C_ No )
143 simplrl 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  a e. A )
144 143 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  a e. A )
145 19 142 144 20 mp3an2i 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( bday ` a ) e. ( bday " A ) )
146 elssuni 
 |-  ( ( bday ` a ) e. ( bday " A ) -> ( bday ` a ) C_ U. ( bday " A ) )
147 145 146 syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( bday ` a ) C_ U. ( bday " A ) )
148 141 147 eqsstrrd 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  dom a C_ U. ( bday " A ) )
149 127 25 33 3syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( dom a C_ U. ( bday " A ) <-> dom a e. suc U. ( bday " A ) ) )
150 148 149 mpbid 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  dom a e. suc U. ( bday " A ) )
151 simpr 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  a =/= W )
152 nosepon 
 |-  ( ( a e. No /\ W e. No /\ a =/= W ) -> |^| { p e. On | ( a ` p ) =/= ( W ` p ) } e. On )
153 56 64 151 152 syl3anc 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  |^| { p e. On | ( a ` p ) =/= ( W ` p ) } e. On )
154 153 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  |^| { p e. On | ( a ` p ) =/= ( W ` p ) } e. On )
155 eloni 
 |-  ( |^| { p e. On | ( a ` p ) =/= ( W ` p ) } e. On -> Ord |^| { p e. On | ( a ` p ) =/= ( W ` p ) } )
156 ordsuc 
 |-  ( Ord U. ( bday " A ) <-> Ord suc U. ( bday " A ) )
157 31 156 mpbi 
 |-  Ord suc U. ( bday " A )
158 ordtr2 
 |-  ( ( Ord |^| { p e. On | ( a ` p ) =/= ( W ` p ) } /\ Ord suc U. ( bday " A ) ) -> ( ( |^| { p e. On | ( a ` p ) =/= ( W ` p ) } C_ dom a /\ dom a e. suc U. ( bday " A ) ) -> |^| { p e. On | ( a ` p ) =/= ( W ` p ) } e. suc U. ( bday " A ) ) )
159 157 158 mpan2 
 |-  ( Ord |^| { p e. On | ( a ` p ) =/= ( W ` p ) } -> ( ( |^| { p e. On | ( a ` p ) =/= ( W ` p ) } C_ dom a /\ dom a e. suc U. ( bday " A ) ) -> |^| { p e. On | ( a ` p ) =/= ( W ` p ) } e. suc U. ( bday " A ) ) )
160 154 155 159 3syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( ( |^| { p e. On | ( a ` p ) =/= ( W ` p ) } C_ dom a /\ dom a e. suc U. ( bday " A ) ) -> |^| { p e. On | ( a ` p ) =/= ( W ` p ) } e. suc U. ( bday " A ) ) )
161 140 150 160 mp2and 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  |^| { p e. On | ( a ` p ) =/= ( W ` p ) } e. suc U. ( bday " A ) )
162 ontri1 
 |-  ( ( dom T e. On /\ |^| { p e. On | ( a ` p ) =/= ( W ` p ) } e. On ) -> ( dom T C_ |^| { p e. On | ( a ` p ) =/= ( W ` p ) } <-> -. |^| { p e. On | ( a ` p ) =/= ( W ` p ) } e. dom T ) )
163 109 153 162 syl2anc 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( dom T C_ |^| { p e. On | ( a ` p ) =/= ( W ` p ) } <-> -. |^| { p e. On | ( a ` p ) =/= ( W ` p ) } e. dom T ) )
164 163 biimpa 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  -. |^| { p e. On | ( a ` p ) =/= ( W ` p ) } e. dom T )
165 161 164 eldifd 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  |^| { p e. On | ( a ` p ) =/= ( W ` p ) } e. ( suc U. ( bday " A ) \ dom T ) )
166 133 136 138 165 fvun2d 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( ( T u. ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) ) ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) = ( ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) )
167 44 fvconst2 
 |-  ( |^| { p e. On | ( a ` p ) =/= ( W ` p ) } e. ( suc U. ( bday " A ) \ dom T ) -> ( ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) = 2o )
168 165 167 syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) = 2o )
169 166 168 eqtrd 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( ( T u. ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) ) ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) = 2o )
170 130 169 syl5eq 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( W ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) = 2o )
171 nosep2o 
 |-  ( ( ( W e. No /\ a e. No /\ W =/= a ) /\ ( W ` |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) = 2o ) -> a
172 126 127 129 170 171 syl31anc 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  a
173 153 155 syl 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  Ord |^| { p e. On | ( a ` p ) =/= ( W ` p ) } )
174 nodmord 
 |-  ( T e. No -> Ord dom T )
175 92 174 syl 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  Ord dom T )
176 ordtri2or 
 |-  ( ( Ord |^| { p e. On | ( a ` p ) =/= ( W ` p ) } /\ Ord dom T ) -> ( |^| { p e. On | ( a ` p ) =/= ( W ` p ) } e. dom T \/ dom T C_ |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) )
177 173 175 176 syl2anc 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  ( |^| { p e. On | ( a ` p ) =/= ( W ` p ) } e. dom T \/ dom T C_ |^| { p e. On | ( a ` p ) =/= ( W ` p ) } ) )
178 125 172 177 mpjaodan 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  a
179 54 178 mpdan 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( a e. A /\ -. T  a
180 179 expr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ a e. A ) -> ( -. T  a
181 8 180 sylbid 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ a e. A ) -> ( A. b e. B a  a
182 181 ralimdva 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) -> ( A. a e. A A. b e. B a  A. a e. A a
183 182 3impia 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  A. a e. A a