Metamath Proof Explorer

Theorem noetasuplem4

Description: Lemma for noeta . When A and B are separated, then Z is a lower bound for B . Part of Theorem 5.1 of Lipparini p. 7-8. (Contributed by Scott Fenton, 7-Dec-2021)

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

Proof

Step Hyp Ref Expression
1 noetasuplem.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 noetasuplem.2 
 |-  Z = ( S u. ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) )
3 ralcom 
 |-  ( A. a e. A A. b e. B a  A. b e. B A. a e. A a
4 simplll 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ b e. B ) -> A C_ No )
5 simpllr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ b e. B ) -> A e. _V )
6 simprl 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) -> B C_ No )
7 6 sselda 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ b e. B ) -> b e. No )
8 1 nosupbnd2 
 |-  ( ( A C_ No /\ A e. _V /\ b e. No ) -> ( A. a e. A a  -. ( b |` dom S )
9 4 5 7 8 syl3anc 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ b e. B ) -> ( A. a e. A a  -. ( b |` dom S )
10 simpl 
 |-  ( ( b e. B /\ -. ( b |` dom S )  b e. B )
11 ssel2 
 |-  ( ( B C_ No /\ b e. B ) -> b e. No )
12 6 10 11 syl2an 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  b e. No )
13 nodmord 
 |-  ( b e. No -> Ord dom b )
14 ordirr 
 |-  ( Ord dom b -> -. dom b e. dom b )
15 12 13 14 3syl 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  -. dom b e. dom b )
16 ssun2 
 |-  suc U. ( bday " B ) C_ ( dom S u. suc U. ( bday " B ) )
17 bdayval 
 |-  ( b e. No -> ( bday ` b ) = dom b )
18 12 17 syl 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( bday ` b ) = dom b )
19 bdayfo 
 |-  bday : No -onto-> On
20 fofn 
 |-  ( bday : No -onto-> On -> bday Fn No )
21 19 20 ax-mp 
 |-  bday Fn No
22 fnfvima 
 |-  ( ( bday Fn No /\ B C_ No /\ b e. B ) -> ( bday ` b ) e. ( bday " B ) )
23 21 22 mp3an1 
 |-  ( ( B C_ No /\ b e. B ) -> ( bday ` b ) e. ( bday " B ) )
24 6 10 23 syl2an 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( bday ` b ) e. ( bday " B ) )
25 18 24 eqeltrrd 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  dom b e. ( bday " B ) )
26 elssuni 
 |-  ( dom b e. ( bday " B ) -> dom b C_ U. ( bday " B ) )
27 25 26 syl 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  dom b C_ U. ( bday " B ) )
28 nodmon 
 |-  ( b e. No -> dom b e. On )
29 imassrn 
 |-  ( bday " B ) C_ ran bday
30 forn 
 |-  ( bday : No -onto-> On -> ran bday = On )
31 19 30 ax-mp 
 |-  ran bday = On
32 29 31 sseqtri 
 |-  ( bday " B ) C_ On
33 ssorduni 
 |-  ( ( bday " B ) C_ On -> Ord U. ( bday " B ) )
34 32 33 ax-mp 
 |-  Ord U. ( bday " B )
35 ordsssuc 
 |-  ( ( dom b e. On /\ Ord U. ( bday " B ) ) -> ( dom b C_ U. ( bday " B ) <-> dom b e. suc U. ( bday " B ) ) )
36 34 35 mpan2 
 |-  ( dom b e. On -> ( dom b C_ U. ( bday " B ) <-> dom b e. suc U. ( bday " B ) ) )
37 12 28 36 3syl 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( dom b C_ U. ( bday " B ) <-> dom b e. suc U. ( bday " B ) ) )
38 27 37 mpbid 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  dom b e. suc U. ( bday " B ) )
39 16 38 sseldi 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  dom b e. ( dom S u. suc U. ( bday " B ) ) )
40 eleq2 
 |-  ( ( dom S u. suc U. ( bday " B ) ) = dom b -> ( dom b e. ( dom S u. suc U. ( bday " B ) ) <-> dom b e. dom b ) )
41 39 40 syl5ibcom 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( ( dom S u. suc U. ( bday " B ) ) = dom b -> dom b e. dom b ) )
42 15 41 mtod 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  -. ( dom S u. suc U. ( bday " B ) ) = dom b )
43 2 dmeqi 
 |-  dom Z = dom ( S u. ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) )
44 dmun 
 |-  dom ( S u. ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) ) = ( dom S u. dom ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) )
45 43 44 eqtri 
 |-  dom Z = ( dom S u. dom ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) )
46 1oex 
 |-  1o e. _V
47 46 snnz 
 |-  { 1o } =/= (/)
48 dmxp 
 |-  ( { 1o } =/= (/) -> dom ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) = ( suc U. ( bday " B ) \ dom S ) )
49 47 48 ax-mp 
 |-  dom ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) = ( suc U. ( bday " B ) \ dom S )
50 49 uneq2i 
 |-  ( dom S u. dom ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) ) = ( dom S u. ( suc U. ( bday " B ) \ dom S ) )
51 undif2 
 |-  ( dom S u. ( suc U. ( bday " B ) \ dom S ) ) = ( dom S u. suc U. ( bday " B ) )
52 45 50 51 3eqtri 
 |-  dom Z = ( dom S u. suc U. ( bday " B ) )
53 dmeq 
 |-  ( Z = b -> dom Z = dom b )
54 52 53 eqtr3id 
 |-  ( Z = b -> ( dom S u. suc U. ( bday " B ) ) = dom b )
55 42 54 nsyl 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  -. Z = b )
56 df-ne 
 |-  ( Z =/= b <-> -. Z = b )
57 notnotr 
 |-  ( -. -. dom ( b |` dom S ) = dom S -> dom ( b |` dom S ) = dom S )
58 simpr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } e. dom S )
59 58 fvresd 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( ( Z |` dom S ) ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) = ( Z ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) )
60 2 reseq1i 
 |-  ( Z |` dom S ) = ( ( S u. ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) ) |` dom S )
61 resundir 
 |-  ( ( S u. ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) ) |` dom S ) = ( ( S |` dom S ) u. ( ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) |` dom S ) )
62 df-res 
 |-  ( ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) |` dom S ) = ( ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) i^i ( dom S X. _V ) )
63 incom 
 |-  ( ( suc U. ( bday " B ) \ dom S ) i^i dom S ) = ( dom S i^i ( suc U. ( bday " B ) \ dom S ) )
64 disjdif 
 |-  ( dom S i^i ( suc U. ( bday " B ) \ dom S ) ) = (/)
65 63 64 eqtri 
 |-  ( ( suc U. ( bday " B ) \ dom S ) i^i dom S ) = (/)
66 xpdisj1 
 |-  ( ( ( suc U. ( bday " B ) \ dom S ) i^i dom S ) = (/) -> ( ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) i^i ( dom S X. _V ) ) = (/) )
67 65 66 ax-mp 
 |-  ( ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) i^i ( dom S X. _V ) ) = (/)
68 62 67 eqtri 
 |-  ( ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) |` dom S ) = (/)
69 68 uneq2i 
 |-  ( ( S |` dom S ) u. ( ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) |` dom S ) ) = ( ( S |` dom S ) u. (/) )
70 un0 
 |-  ( ( S |` dom S ) u. (/) ) = ( S |` dom S )
71 69 70 eqtri 
 |-  ( ( S |` dom S ) u. ( ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) |` dom S ) ) = ( S |` dom S )
72 60 61 71 3eqtri 
 |-  ( Z |` dom S ) = ( S |` dom S )
73 simplll 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( A C_ No /\ A e. _V ) )
74 1 nosupno 
 |-  ( ( A C_ No /\ A e. _V ) -> S e. No )
75 73 74 syl 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  S e. No )
76 75 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  S e. No )
77 nofun 
 |-  ( S e. No -> Fun S )
78 76 77 syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Fun S )
79 funrel 
 |-  ( Fun S -> Rel S )
80 resdm 
 |-  ( Rel S -> ( S |` dom S ) = S )
81 78 79 80 3syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( S |` dom S ) = S )
82 72 81 syl5eq 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( Z |` dom S ) = S )
83 82 fveq1d 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( ( Z |` dom S ) ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) = ( S ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) )
84 59 83 eqtr3d 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( Z ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) = ( S ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) )
85 simp-4l 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  A C_ No )
86 simp-4r 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  A e. _V )
87 simplrr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  B e. _V )
88 87 adantr 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  B e. _V )
89 1 2 noetasuplem1 
 |-  ( ( A C_ No /\ A e. _V /\ B e. _V ) -> Z e. No )
90 85 86 88 89 syl3anc 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Z e. No )
91 90 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Z e. No )
92 12 adantr 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  b e. No )
93 92 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  b e. No )
94 simplr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Z =/= b )
95 nosepne 
 |-  ( ( Z e. No /\ b e. No /\ Z =/= b ) -> ( Z ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) =/= ( b ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) )
96 91 93 94 95 syl3anc 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( Z ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) =/= ( b ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) )
97 84 96 eqnetrrd 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( S ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) =/= ( b ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) )
98 58 fvresd 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( ( b |` dom S ) ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) = ( b ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) )
99 97 98 neeqtrrd 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( S ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) =/= ( ( b |` dom S ) ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) )
100 fveq2 
 |-  ( q = |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } -> ( ( b |` dom S ) ` q ) = ( ( b |` dom S ) ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) )
101 fveq2 
 |-  ( q = |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } -> ( S ` q ) = ( S ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) )
102 100 101 neeq12d 
 |-  ( q = |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } -> ( ( ( b |` dom S ) ` q ) =/= ( S ` q ) <-> ( ( b |` dom S ) ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) =/= ( S ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) ) )
103 df-ne 
 |-  ( ( ( b |` dom S ) ` q ) =/= ( S ` q ) <-> -. ( ( b |` dom S ) ` q ) = ( S ` q ) )
104 necom 
 |-  ( ( ( b |` dom S ) ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) =/= ( S ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) <-> ( S ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) =/= ( ( b |` dom S ) ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) )
105 102 103 104 3bitr3g 
 |-  ( q = |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } -> ( -. ( ( b |` dom S ) ` q ) = ( S ` q ) <-> ( S ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) =/= ( ( b |` dom S ) ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) ) )
106 105 rspcev 
 |-  ( ( |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } e. dom S /\ ( S ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) =/= ( ( b |` dom S ) ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) ) -> E. q e. dom S -. ( ( b |` dom S ) ` q ) = ( S ` q ) )
107 58 99 106 syl2anc 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  E. q e. dom S -. ( ( b |` dom S ) ` q ) = ( S ` q ) )
108 rexeq 
 |-  ( dom ( b |` dom S ) = dom S -> ( E. q e. dom ( b |` dom S ) -. ( ( b |` dom S ) ` q ) = ( S ` q ) <-> E. q e. dom S -. ( ( b |` dom S ) ` q ) = ( S ` q ) ) )
109 107 108 syl5ibrcom 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( dom ( b |` dom S ) = dom S -> E. q e. dom ( b |` dom S ) -. ( ( b |` dom S ) ` q ) = ( S ` q ) ) )
110 rexnal 
 |-  ( E. q e. dom ( b |` dom S ) -. ( ( b |` dom S ) ` q ) = ( S ` q ) <-> -. A. q e. dom ( b |` dom S ) ( ( b |` dom S ) ` q ) = ( S ` q ) )
111 109 110 syl6ib 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( dom ( b |` dom S ) = dom S -> -. A. q e. dom ( b |` dom S ) ( ( b |` dom S ) ` q ) = ( S ` q ) ) )
112 57 111 syl5 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( -. -. dom ( b |` dom S ) = dom S -> -. A. q e. dom ( b |` dom S ) ( ( b |` dom S ) ` q ) = ( S ` q ) ) )
113 112 orrd 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( -. dom ( b |` dom S ) = dom S \/ -. A. q e. dom ( b |` dom S ) ( ( b |` dom S ) ` q ) = ( S ` q ) ) )
114 nofun 
 |-  ( b e. No -> Fun b )
115 funres 
 |-  ( Fun b -> Fun ( b |` dom S ) )
116 93 114 115 3syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Fun ( b |` dom S ) )
117 eqfunfv 
 |-  ( ( Fun ( b |` dom S ) /\ Fun S ) -> ( ( b |` dom S ) = S <-> ( dom ( b |` dom S ) = dom S /\ A. q e. dom ( b |` dom S ) ( ( b |` dom S ) ` q ) = ( S ` q ) ) ) )
118 116 78 117 syl2anc 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( ( b |` dom S ) = S <-> ( dom ( b |` dom S ) = dom S /\ A. q e. dom ( b |` dom S ) ( ( b |` dom S ) ` q ) = ( S ` q ) ) ) )
119 ianor 
 |-  ( -. ( dom ( b |` dom S ) = dom S /\ A. q e. dom ( b |` dom S ) ( ( b |` dom S ) ` q ) = ( S ` q ) ) <-> ( -. dom ( b |` dom S ) = dom S \/ -. A. q e. dom ( b |` dom S ) ( ( b |` dom S ) ` q ) = ( S ` q ) ) )
120 119 con1bii 
 |-  ( -. ( -. dom ( b |` dom S ) = dom S \/ -. A. q e. dom ( b |` dom S ) ( ( b |` dom S ) ` q ) = ( S ` q ) ) <-> ( dom ( b |` dom S ) = dom S /\ A. q e. dom ( b |` dom S ) ( ( b |` dom S ) ` q ) = ( S ` q ) ) )
121 118 120 bitr4di 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( ( b |` dom S ) = S <-> -. ( -. dom ( b |` dom S ) = dom S \/ -. A. q e. dom ( b |` dom S ) ( ( b |` dom S ) ` q ) = ( S ` q ) ) ) )
122 121 con2bid 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( ( -. dom ( b |` dom S ) = dom S \/ -. A. q e. dom ( b |` dom S ) ( ( b |` dom S ) ` q ) = ( S ` q ) ) <-> -. ( b |` dom S ) = S ) )
123 113 122 mpbid 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  -. ( b |` dom S ) = S )
124 123 pm2.21d 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( ( b |` dom S ) = S -> Z
125 82 breq1d 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( ( Z |` dom S )  S
126 nodmon 
 |-  ( S e. No -> dom S e. On )
127 76 126 syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  dom S e. On )
128 sltres 
 |-  ( ( Z e. No /\ b e. No /\ dom S e. On ) -> ( ( Z |` dom S )  Z
129 91 93 127 128 syl3anc 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( ( Z |` dom S )  Z
130 125 129 sylbird 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( S  Z
131 simplrr 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  -. ( b |` dom S )
132 131 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  -. ( b |` dom S )
133 noreson 
 |-  ( ( b e. No /\ dom S e. On ) -> ( b |` dom S ) e. No )
134 93 127 133 syl2anc 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( b |` dom S ) e. No )
135 sltso 
 |-
136 sotric 
 |-  ( (  ( ( b |` dom S )  -. ( ( b |` dom S ) = S \/ S
137 135 136 mpan 
 |-  ( ( ( b |` dom S ) e. No /\ S e. No ) -> ( ( b |` dom S )  -. ( ( b |` dom S ) = S \/ S
138 134 76 137 syl2anc 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( ( b |` dom S )  -. ( ( b |` dom S ) = S \/ S
139 138 con2bid 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( ( ( b |` dom S ) = S \/ S  -. ( b |` dom S )
140 132 139 mpbird 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( ( b |` dom S ) = S \/ S
141 124 130 140 mpjaod 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Z
142 90 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Z e. No )
143 92 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  b e. No )
144 simplr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Z =/= b )
145 2 fveq1i 
 |-  ( Z ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) = ( ( S u. ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) ) ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } )
146 simp-4l 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( A C_ No /\ A e. _V ) )
147 146 74 77 3syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Fun S )
148 funfn 
 |-  ( Fun S <-> S Fn dom S )
149 147 148 sylib 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  S Fn dom S )
150 46 fconst 
 |-  ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) : ( suc U. ( bday " B ) \ dom S ) --> { 1o }
151 ffn 
 |-  ( ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) : ( suc U. ( bday " B ) \ dom S ) --> { 1o } -> ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) Fn ( suc U. ( bday " B ) \ dom S ) )
152 150 151 ax-mp 
 |-  ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) Fn ( suc U. ( bday " B ) \ dom S )
153 152 a1i 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) Fn ( suc U. ( bday " B ) \ dom S ) )
154 64 a1i 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( dom S i^i ( suc U. ( bday " B ) \ dom S ) ) = (/) )
155 necom 
 |-  ( ( Z ` p ) =/= ( b ` p ) <-> ( b ` p ) =/= ( Z ` p ) )
156 155 rabbii 
 |-  { p e. On | ( Z ` p ) =/= ( b ` p ) } = { p e. On | ( b ` p ) =/= ( Z ` p ) }
157 156 inteqi 
 |-  |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } = |^| { p e. On | ( b ` p ) =/= ( Z ` p ) }
158 144 necomd 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  b =/= Z )
159 nosepssdm 
 |-  ( ( b e. No /\ Z e. No /\ b =/= Z ) -> |^| { p e. On | ( b ` p ) =/= ( Z ` p ) } C_ dom b )
160 143 142 158 159 syl3anc 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  |^| { p e. On | ( b ` p ) =/= ( Z ` p ) } C_ dom b )
161 157 160 eqsstrid 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } C_ dom b )
162 143 17 syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( bday ` b ) = dom b )
163 simplrl 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  B C_ No )
164 163 adantr 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  B C_ No )
165 164 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  B C_ No )
166 simplrl 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  b e. B )
167 166 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  b e. B )
168 165 167 23 syl2anc 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( bday ` b ) e. ( bday " B ) )
169 162 168 eqeltrrd 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  dom b e. ( bday " B ) )
170 169 26 syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  dom b C_ U. ( bday " B ) )
171 143 28 36 3syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( dom b C_ U. ( bday " B ) <-> dom b e. suc U. ( bday " B ) ) )
172 170 171 mpbid 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  dom b e. suc U. ( bday " B ) )
173 nosepon 
 |-  ( ( Z e. No /\ b e. No /\ Z =/= b ) -> |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } e. On )
174 142 143 144 173 syl3anc 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } e. On )
175 eloni 
 |-  ( |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } e. On -> Ord |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } )
176 ordsuc 
 |-  ( Ord U. ( bday " B ) <-> Ord suc U. ( bday " B ) )
177 34 176 mpbi 
 |-  Ord suc U. ( bday " B )
178 ordtr2 
 |-  ( ( Ord |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } /\ Ord suc U. ( bday " B ) ) -> ( ( |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } C_ dom b /\ dom b e. suc U. ( bday " B ) ) -> |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } e. suc U. ( bday " B ) ) )
179 177 178 mpan2 
 |-  ( Ord |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } -> ( ( |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } C_ dom b /\ dom b e. suc U. ( bday " B ) ) -> |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } e. suc U. ( bday " B ) ) )
180 174 175 179 3syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( ( |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } C_ dom b /\ dom b e. suc U. ( bday " B ) ) -> |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } e. suc U. ( bday " B ) ) )
181 161 172 180 mp2and 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } e. suc U. ( bday " B ) )
182 simpr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  dom S C_ |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } )
183 146 74 126 3syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  dom S e. On )
184 ontri1 
 |-  ( ( dom S e. On /\ |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } e. On ) -> ( dom S C_ |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } <-> -. |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } e. dom S ) )
185 183 174 184 syl2anc 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( dom S C_ |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } <-> -. |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } e. dom S ) )
186 182 185 mpbid 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  -. |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } e. dom S )
187 181 186 eldifd 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } e. ( suc U. ( bday " B ) \ dom S ) )
188 fvun2 
 |-  ( ( S Fn dom S /\ ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) Fn ( suc U. ( bday " B ) \ dom S ) /\ ( ( dom S i^i ( suc U. ( bday " B ) \ dom S ) ) = (/) /\ |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } e. ( suc U. ( bday " B ) \ dom S ) ) ) -> ( ( S u. ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) ) ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) = ( ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) )
189 149 153 154 187 188 syl112anc 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( ( S u. ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) ) ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) = ( ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) )
190 145 189 syl5eq 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( Z ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) = ( ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) )
191 46 fvconst2 
 |-  ( |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } e. ( suc U. ( bday " B ) \ dom S ) -> ( ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) = 1o )
192 187 191 syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) = 1o )
193 190 192 eqtrd 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( Z ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) = 1o )
194 nosep1o 
 |-  ( ( ( Z e. No /\ b e. No /\ Z =/= b ) /\ ( Z ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) = 1o ) -> Z
195 142 143 144 193 194 syl31anc 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Z
196 simpr 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Z =/= b )
197 90 92 196 173 syl3anc 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } e. On )
198 197 175 syl 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Ord |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } )
199 nodmord 
 |-  ( S e. No -> Ord dom S )
200 73 74 199 3syl 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Ord dom S )
201 ordtri2or 
 |-  ( ( Ord |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } /\ Ord dom S ) -> ( |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } e. dom S \/ dom S C_ |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) )
202 198 200 201 syl2anc 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } e. dom S \/ dom S C_ |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) )
203 141 195 202 mpjaodan 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Z
204 203 ex 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( Z =/= b -> Z
205 56 204 syl5bir 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( -. Z = b -> Z
206 55 205 mpd 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Z
207 206 expr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ b e. B ) -> ( -. ( b |` dom S )  Z
208 9 207 sylbid 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ b e. B ) -> ( A. a e. A a  Z
209 208 ralimdva 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) -> ( A. b e. B A. a e. A a  A. b e. B Z
210 3 209 syl5bi 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) -> ( A. a e. A A. b e. B a  A. b e. B Z
211 210 3impia 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  A. b e. B Z