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 sselid 
 |-  ( ( ( ( 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 disjdifr 
 |-  ( ( suc U. ( bday " B ) \ dom S ) i^i dom S ) = (/)
64 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 ) ) = (/) )
65 63 64 ax-mp 
 |-  ( ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) i^i ( dom S X. _V ) ) = (/)
66 62 65 eqtri 
 |-  ( ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) |` dom S ) = (/)
67 66 uneq2i 
 |-  ( ( S |` dom S ) u. ( ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) |` dom S ) ) = ( ( S |` dom S ) u. (/) )
68 un0 
 |-  ( ( S |` dom S ) u. (/) ) = ( S |` dom S )
69 67 68 eqtri 
 |-  ( ( S |` dom S ) u. ( ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) |` dom S ) ) = ( S |` dom S )
70 60 61 69 3eqtri 
 |-  ( Z |` dom S ) = ( S |` dom S )
71 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 ) )
72 1 nosupno 
 |-  ( ( A C_ No /\ A e. _V ) -> S e. No )
73 71 72 syl 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  S e. No )
74 73 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  S e. No )
75 nofun 
 |-  ( S e. No -> Fun S )
76 74 75 syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Fun S )
77 funrel 
 |-  ( Fun S -> Rel S )
78 resdm 
 |-  ( Rel S -> ( S |` dom S ) = S )
79 76 77 78 3syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( S |` dom S ) = S )
80 70 79 eqtrid 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( Z |` dom S ) = S )
81 80 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 ) } ) )
82 59 81 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 ) } ) )
83 simp-4l 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  A C_ No )
84 simp-4r 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  A e. _V )
85 simplrr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  B e. _V )
86 85 adantr 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  B e. _V )
87 1 2 noetasuplem1 
 |-  ( ( A C_ No /\ A e. _V /\ B e. _V ) -> Z e. No )
88 83 84 86 87 syl3anc 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Z e. No )
89 88 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Z e. No )
90 12 adantr 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  b e. No )
91 90 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  b e. No )
92 simplr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Z =/= b )
93 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 ) } ) )
94 89 91 92 93 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 ) } ) )
95 82 94 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 ) } ) )
96 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 ) } ) )
97 95 96 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 ) } ) )
98 fveq2 
 |-  ( q = |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } -> ( ( b |` dom S ) ` q ) = ( ( b |` dom S ) ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) )
99 fveq2 
 |-  ( q = |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } -> ( S ` q ) = ( S ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) )
100 98 99 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 ) } ) ) )
101 df-ne 
 |-  ( ( ( b |` dom S ) ` q ) =/= ( S ` q ) <-> -. ( ( b |` dom S ) ` q ) = ( S ` q ) )
102 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 ) } ) )
103 100 101 102 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 ) } ) ) )
104 103 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 ) )
105 58 97 104 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 ) )
106 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 ) ) )
107 105 106 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 ) ) )
108 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 ) )
109 107 108 imbitrdi 
 |-  ( ( ( ( ( ( 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 ) ) )
110 57 109 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 ) ) )
111 110 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 ) ) )
112 nofun 
 |-  ( b e. No -> Fun b )
113 funres 
 |-  ( Fun b -> Fun ( b |` dom S ) )
114 91 112 113 3syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Fun ( b |` dom S ) )
115 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 ) ) ) )
116 114 76 115 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 ) ) ) )
117 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 ) ) )
118 117 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 ) ) )
119 116 118 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 ) ) ) )
120 119 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 ) )
121 111 120 mpbid 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  -. ( b |` dom S ) = S )
122 121 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
123 80 breq1d 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( ( Z |` dom S )  S
124 nodmon 
 |-  ( S e. No -> dom S e. On )
125 74 124 syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  dom S e. On )
126 sltres 
 |-  ( ( Z e. No /\ b e. No /\ dom S e. On ) -> ( ( Z |` dom S )  Z
127 89 91 125 126 syl3anc 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( ( Z |` dom S )  Z
128 123 127 sylbird 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( S  Z
129 simplrr 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  -. ( b |` dom S )
130 129 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  -. ( b |` dom S )
131 noreson 
 |-  ( ( b e. No /\ dom S e. On ) -> ( b |` dom S ) e. No )
132 91 125 131 syl2anc 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( b |` dom S ) e. No )
133 sltso 
 |-
134 sotric 
 |-  ( (  ( ( b |` dom S )  -. ( ( b |` dom S ) = S \/ S
135 133 134 mpan 
 |-  ( ( ( b |` dom S ) e. No /\ S e. No ) -> ( ( b |` dom S )  -. ( ( b |` dom S ) = S \/ S
136 132 74 135 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
137 136 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 )
138 130 137 mpbird 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( ( b |` dom S ) = S \/ S
139 122 128 138 mpjaod 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Z
140 88 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Z e. No )
141 90 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  b e. No )
142 simplr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Z =/= b )
143 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 ) } )
144 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 ) )
145 144 72 75 3syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Fun S )
146 funfn 
 |-  ( Fun S <-> S Fn dom S )
147 145 146 sylib 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  S Fn dom S )
148 46 fconst 
 |-  ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) : ( suc U. ( bday " B ) \ dom S ) --> { 1o }
149 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 ) )
150 148 149 ax-mp 
 |-  ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) Fn ( suc U. ( bday " B ) \ dom S )
151 150 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 ) )
152 disjdif 
 |-  ( dom S i^i ( 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 )  ( dom S i^i ( suc U. ( bday " B ) \ dom S ) ) = (/) )
154 necom 
 |-  ( ( Z ` p ) =/= ( b ` p ) <-> ( b ` p ) =/= ( Z ` p ) )
155 154 rabbii 
 |-  { p e. On | ( Z ` p ) =/= ( b ` p ) } = { p e. On | ( b ` p ) =/= ( Z ` p ) }
156 155 inteqi 
 |-  |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } = |^| { p e. On | ( b ` p ) =/= ( Z ` p ) }
157 142 necomd 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  b =/= Z )
158 nosepssdm 
 |-  ( ( b e. No /\ Z e. No /\ b =/= Z ) -> |^| { p e. On | ( b ` p ) =/= ( Z ` p ) } C_ dom b )
159 141 140 157 158 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 )
160 156 159 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 )
161 141 17 syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( bday ` b ) = dom b )
162 simplrl 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  B C_ No )
163 162 adantr 
 |-  ( ( ( ( ( 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 simplrl 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  b e. B )
166 165 adantr 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  b e. B )
167 164 166 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 ) )
168 161 167 eqeltrrd 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  dom b e. ( bday " B ) )
169 168 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 ) )
170 141 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 ) ) )
171 169 170 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 ) )
172 nosepon 
 |-  ( ( Z e. No /\ b e. No /\ Z =/= b ) -> |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } e. On )
173 140 141 142 172 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 )
174 eloni 
 |-  ( |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } e. On -> Ord |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } )
175 ordsuc 
 |-  ( Ord U. ( bday " B ) <-> Ord suc U. ( bday " B ) )
176 34 175 mpbi 
 |-  Ord suc U. ( bday " B )
177 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 ) ) )
178 176 177 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 ) ) )
179 173 174 178 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 ) ) )
180 160 171 179 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 ) )
181 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 ) } )
182 144 72 124 3syl 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  dom S e. On )
183 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 ) )
184 182 173 183 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 ) )
185 181 184 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 )
186 180 185 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 ) )
187 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 ) } ) )
188 147 151 153 186 187 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 ) } ) )
189 143 188 eqtrid 
 |-  ( ( ( ( ( ( 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 ) } ) )
190 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 )
191 186 190 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 )
192 189 191 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 )
193 nosep1o 
 |-  ( ( ( Z e. No /\ b e. No /\ Z =/= b ) /\ ( Z ` |^| { p e. On | ( Z ` p ) =/= ( b ` p ) } ) = 1o ) -> Z
194 140 141 142 192 193 syl31anc 
 |-  ( ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Z
195 simpr 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Z =/= b )
196 88 90 195 172 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 )
197 196 174 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 ) } )
198 nodmord 
 |-  ( S e. No -> Ord dom S )
199 71 72 198 3syl 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Ord dom S )
200 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 ) } ) )
201 197 199 200 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 ) } ) )
202 139 194 201 mpjaodan 
 |-  ( ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Z
203 202 ex 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( Z =/= b -> Z
204 56 203 biimtrrid 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  ( -. Z = b -> Z
205 55 204 mpd 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( b e. B /\ -. ( b |` dom S )  Z
206 205 expr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ b e. B ) -> ( -. ( b |` dom S )  Z
207 9 206 sylbid 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ b e. B ) -> ( A. a e. A a  Z
208 207 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
209 3 208 biimtrid 
 |-  ( ( ( 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
210 209 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