Metamath Proof Explorer

Theorem addsuniflem

Description: Lemma for addsunif . State the whole theorem with extra distinct variable conditions. (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Hypotheses addsuniflem.1 
|- ( ph -> L <
addsuniflem.2 
|- ( ph -> M <
addsuniflem.3 
|- ( ph -> A = ( L |s R ) )
addsuniflem.4 
|- ( ph -> B = ( M |s S ) )
Assertion addsuniflem 
|- ( ph -> ( A +s B ) = ( ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) |s ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) ) )

Proof

Step Hyp Ref Expression
1 addsuniflem.1 
 |-  ( ph -> L <
2 addsuniflem.2 
 |-  ( ph -> M <
3 addsuniflem.3 
 |-  ( ph -> A = ( L |s R ) )
4 addsuniflem.4 
 |-  ( ph -> B = ( M |s S ) )
5 1 scutcld 
 |-  ( ph -> ( L |s R ) e. No )
6 3 5 eqeltrd 
 |-  ( ph -> A e. No )
7 2 scutcld 
 |-  ( ph -> ( M |s S ) e. No )
8 4 7 eqeltrd 
 |-  ( ph -> B e. No )
9 addsval2 
 |-  ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) |s ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) ) )
10 6 8 9 syl2anc 
 |-  ( ph -> ( A +s B ) = ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) |s ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) ) )
11 6 8 addscut 
 |-  ( ph -> ( ( A +s B ) e. No /\ ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) <
12 11 simp2d 
 |-  ( ph -> ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) <
13 11 simp3d 
 |-  ( ph -> { ( A +s B ) } <
14 ovex 
 |-  ( A +s B ) e. _V
15 14 snnz 
 |-  { ( A +s B ) } =/= (/)
16 sslttr 
 |-  ( ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) < ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) <
17 15 16 mp3an3 
 |-  ( ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) < ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) <
18 12 13 17 syl2anc 
 |-  ( ph -> ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) <
19 1 3 cofcutr1d 
 |-  ( ph -> A. p e. ( _Left ` A ) E. l e. L p <_s l )
20 leftssno 
 |-  ( _Left ` A ) C_ No
21 20 sseli 
 |-  ( p e. ( _Left ` A ) -> p e. No )
22 21 ad2antlr 
 |-  ( ( ( ph /\ p e. ( _Left ` A ) ) /\ l e. L ) -> p e. No )
23 ssltss1 
 |-  ( L < L C_ No )
24 1 23 syl 
 |-  ( ph -> L C_ No )
25 24 adantr 
 |-  ( ( ph /\ p e. ( _Left ` A ) ) -> L C_ No )
26 25 sselda 
 |-  ( ( ( ph /\ p e. ( _Left ` A ) ) /\ l e. L ) -> l e. No )
27 8 ad2antrr 
 |-  ( ( ( ph /\ p e. ( _Left ` A ) ) /\ l e. L ) -> B e. No )
28 22 26 27 sleadd1d 
 |-  ( ( ( ph /\ p e. ( _Left ` A ) ) /\ l e. L ) -> ( p <_s l <-> ( p +s B ) <_s ( l +s B ) ) )
29 28 rexbidva 
 |-  ( ( ph /\ p e. ( _Left ` A ) ) -> ( E. l e. L p <_s l <-> E. l e. L ( p +s B ) <_s ( l +s B ) ) )
30 29 ralbidva 
 |-  ( ph -> ( A. p e. ( _Left ` A ) E. l e. L p <_s l <-> A. p e. ( _Left ` A ) E. l e. L ( p +s B ) <_s ( l +s B ) ) )
31 19 30 mpbid 
 |-  ( ph -> A. p e. ( _Left ` A ) E. l e. L ( p +s B ) <_s ( l +s B ) )
32 eqeq1 
 |-  ( y = s -> ( y = ( l +s B ) <-> s = ( l +s B ) ) )
33 32 rexbidv 
 |-  ( y = s -> ( E. l e. L y = ( l +s B ) <-> E. l e. L s = ( l +s B ) ) )
34 33 rexab 
 |-  ( E. s e. { y | E. l e. L y = ( l +s B ) } ( p +s B ) <_s s <-> E. s ( E. l e. L s = ( l +s B ) /\ ( p +s B ) <_s s ) )
35 rexcom4 
 |-  ( E. l e. L E. s ( s = ( l +s B ) /\ ( p +s B ) <_s s ) <-> E. s E. l e. L ( s = ( l +s B ) /\ ( p +s B ) <_s s ) )
36 ovex 
 |-  ( l +s B ) e. _V
37 breq2 
 |-  ( s = ( l +s B ) -> ( ( p +s B ) <_s s <-> ( p +s B ) <_s ( l +s B ) ) )
38 36 37 ceqsexv 
 |-  ( E. s ( s = ( l +s B ) /\ ( p +s B ) <_s s ) <-> ( p +s B ) <_s ( l +s B ) )
39 38 rexbii 
 |-  ( E. l e. L E. s ( s = ( l +s B ) /\ ( p +s B ) <_s s ) <-> E. l e. L ( p +s B ) <_s ( l +s B ) )
40 r19.41v 
 |-  ( E. l e. L ( s = ( l +s B ) /\ ( p +s B ) <_s s ) <-> ( E. l e. L s = ( l +s B ) /\ ( p +s B ) <_s s ) )
41 40 exbii 
 |-  ( E. s E. l e. L ( s = ( l +s B ) /\ ( p +s B ) <_s s ) <-> E. s ( E. l e. L s = ( l +s B ) /\ ( p +s B ) <_s s ) )
42 35 39 41 3bitr3ri 
 |-  ( E. s ( E. l e. L s = ( l +s B ) /\ ( p +s B ) <_s s ) <-> E. l e. L ( p +s B ) <_s ( l +s B ) )
43 34 42 bitri 
 |-  ( E. s e. { y | E. l e. L y = ( l +s B ) } ( p +s B ) <_s s <-> E. l e. L ( p +s B ) <_s ( l +s B ) )
44 ssun1 
 |-  { y | E. l e. L y = ( l +s B ) } C_ ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } )
45 ssrexv 
 |-  ( { y | E. l e. L y = ( l +s B ) } C_ ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) -> ( E. s e. { y | E. l e. L y = ( l +s B ) } ( p +s B ) <_s s -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s ) )
46 44 45 ax-mp 
 |-  ( E. s e. { y | E. l e. L y = ( l +s B ) } ( p +s B ) <_s s -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s )
47 43 46 sylbir 
 |-  ( E. l e. L ( p +s B ) <_s ( l +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s )
48 47 ralimi 
 |-  ( A. p e. ( _Left ` A ) E. l e. L ( p +s B ) <_s ( l +s B ) -> A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s )
49 31 48 syl 
 |-  ( ph -> A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s )
50 2 4 cofcutr1d 
 |-  ( ph -> A. q e. ( _Left ` B ) E. m e. M q <_s m )
51 leftssno 
 |-  ( _Left ` B ) C_ No
52 51 sseli 
 |-  ( q e. ( _Left ` B ) -> q e. No )
53 52 ad2antlr 
 |-  ( ( ( ph /\ q e. ( _Left ` B ) ) /\ m e. M ) -> q e. No )
54 ssltss1 
 |-  ( M < M C_ No )
55 2 54 syl 
 |-  ( ph -> M C_ No )
56 55 adantr 
 |-  ( ( ph /\ q e. ( _Left ` B ) ) -> M C_ No )
57 56 sselda 
 |-  ( ( ( ph /\ q e. ( _Left ` B ) ) /\ m e. M ) -> m e. No )
58 6 ad2antrr 
 |-  ( ( ( ph /\ q e. ( _Left ` B ) ) /\ m e. M ) -> A e. No )
59 53 57 58 sleadd2d 
 |-  ( ( ( ph /\ q e. ( _Left ` B ) ) /\ m e. M ) -> ( q <_s m <-> ( A +s q ) <_s ( A +s m ) ) )
60 59 rexbidva 
 |-  ( ( ph /\ q e. ( _Left ` B ) ) -> ( E. m e. M q <_s m <-> E. m e. M ( A +s q ) <_s ( A +s m ) ) )
61 60 ralbidva 
 |-  ( ph -> ( A. q e. ( _Left ` B ) E. m e. M q <_s m <-> A. q e. ( _Left ` B ) E. m e. M ( A +s q ) <_s ( A +s m ) ) )
62 50 61 mpbid 
 |-  ( ph -> A. q e. ( _Left ` B ) E. m e. M ( A +s q ) <_s ( A +s m ) )
63 eqeq1 
 |-  ( z = s -> ( z = ( A +s m ) <-> s = ( A +s m ) ) )
64 63 rexbidv 
 |-  ( z = s -> ( E. m e. M z = ( A +s m ) <-> E. m e. M s = ( A +s m ) ) )
65 64 rexab 
 |-  ( E. s e. { z | E. m e. M z = ( A +s m ) } ( A +s q ) <_s s <-> E. s ( E. m e. M s = ( A +s m ) /\ ( A +s q ) <_s s ) )
66 rexcom4 
 |-  ( E. m e. M E. s ( s = ( A +s m ) /\ ( A +s q ) <_s s ) <-> E. s E. m e. M ( s = ( A +s m ) /\ ( A +s q ) <_s s ) )
67 ovex 
 |-  ( A +s m ) e. _V
68 breq2 
 |-  ( s = ( A +s m ) -> ( ( A +s q ) <_s s <-> ( A +s q ) <_s ( A +s m ) ) )
69 67 68 ceqsexv 
 |-  ( E. s ( s = ( A +s m ) /\ ( A +s q ) <_s s ) <-> ( A +s q ) <_s ( A +s m ) )
70 69 rexbii 
 |-  ( E. m e. M E. s ( s = ( A +s m ) /\ ( A +s q ) <_s s ) <-> E. m e. M ( A +s q ) <_s ( A +s m ) )
71 r19.41v 
 |-  ( E. m e. M ( s = ( A +s m ) /\ ( A +s q ) <_s s ) <-> ( E. m e. M s = ( A +s m ) /\ ( A +s q ) <_s s ) )
72 71 exbii 
 |-  ( E. s E. m e. M ( s = ( A +s m ) /\ ( A +s q ) <_s s ) <-> E. s ( E. m e. M s = ( A +s m ) /\ ( A +s q ) <_s s ) )
73 66 70 72 3bitr3ri 
 |-  ( E. s ( E. m e. M s = ( A +s m ) /\ ( A +s q ) <_s s ) <-> E. m e. M ( A +s q ) <_s ( A +s m ) )
74 65 73 bitri 
 |-  ( E. s e. { z | E. m e. M z = ( A +s m ) } ( A +s q ) <_s s <-> E. m e. M ( A +s q ) <_s ( A +s m ) )
75 ssun2 
 |-  { z | E. m e. M z = ( A +s m ) } C_ ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } )
76 ssrexv 
 |-  ( { z | E. m e. M z = ( A +s m ) } C_ ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) -> ( E. s e. { z | E. m e. M z = ( A +s m ) } ( A +s q ) <_s s -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) )
77 75 76 ax-mp 
 |-  ( E. s e. { z | E. m e. M z = ( A +s m ) } ( A +s q ) <_s s -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s )
78 74 77 sylbir 
 |-  ( E. m e. M ( A +s q ) <_s ( A +s m ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s )
79 78 ralimi 
 |-  ( A. q e. ( _Left ` B ) E. m e. M ( A +s q ) <_s ( A +s m ) -> A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s )
80 62 79 syl 
 |-  ( ph -> A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s )
81 ralunb 
 |-  ( A. r e. ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> ( A. r e. { a | E. p e. ( _Left ` A ) a = ( p +s B ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s /\ A. r e. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) )
82 eqeq1 
 |-  ( a = r -> ( a = ( p +s B ) <-> r = ( p +s B ) ) )
83 82 rexbidv 
 |-  ( a = r -> ( E. p e. ( _Left ` A ) a = ( p +s B ) <-> E. p e. ( _Left ` A ) r = ( p +s B ) ) )
84 83 ralab 
 |-  ( A. r e. { a | E. p e. ( _Left ` A ) a = ( p +s B ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> A. r ( E. p e. ( _Left ` A ) r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) )
85 ralcom4 
 |-  ( A. p e. ( _Left ` A ) A. r ( r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. r A. p e. ( _Left ` A ) ( r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) )
86 ovex 
 |-  ( p +s B ) e. _V
87 breq1 
 |-  ( r = ( p +s B ) -> ( r <_s s <-> ( p +s B ) <_s s ) )
88 87 rexbidv 
 |-  ( r = ( p +s B ) -> ( E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s ) )
89 86 88 ceqsalv 
 |-  ( A. r ( r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s )
90 89 ralbii 
 |-  ( A. p e. ( _Left ` A ) A. r ( r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s )
91 r19.23v 
 |-  ( A. p e. ( _Left ` A ) ( r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> ( E. p e. ( _Left ` A ) r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) )
92 91 albii 
 |-  ( A. r A. p e. ( _Left ` A ) ( r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. r ( E. p e. ( _Left ` A ) r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) )
93 85 90 92 3bitr3ri 
 |-  ( A. r ( E. p e. ( _Left ` A ) r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s )
94 84 93 bitri 
 |-  ( A. r e. { a | E. p e. ( _Left ` A ) a = ( p +s B ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s )
95 eqeq1 
 |-  ( b = r -> ( b = ( A +s q ) <-> r = ( A +s q ) ) )
96 95 rexbidv 
 |-  ( b = r -> ( E. q e. ( _Left ` B ) b = ( A +s q ) <-> E. q e. ( _Left ` B ) r = ( A +s q ) ) )
97 96 ralab 
 |-  ( A. r e. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> A. r ( E. q e. ( _Left ` B ) r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) )
98 ralcom4 
 |-  ( A. q e. ( _Left ` B ) A. r ( r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. r A. q e. ( _Left ` B ) ( r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) )
99 ovex 
 |-  ( A +s q ) e. _V
100 breq1 
 |-  ( r = ( A +s q ) -> ( r <_s s <-> ( A +s q ) <_s s ) )
101 100 rexbidv 
 |-  ( r = ( A +s q ) -> ( E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) )
102 99 101 ceqsalv 
 |-  ( A. r ( r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s )
103 102 ralbii 
 |-  ( A. q e. ( _Left ` B ) A. r ( r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s )
104 r19.23v 
 |-  ( A. q e. ( _Left ` B ) ( r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> ( E. q e. ( _Left ` B ) r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) )
105 104 albii 
 |-  ( A. r A. q e. ( _Left ` B ) ( r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. r ( E. q e. ( _Left ` B ) r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) )
106 98 103 105 3bitr3ri 
 |-  ( A. r ( E. q e. ( _Left ` B ) r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s )
107 97 106 bitri 
 |-  ( A. r e. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s )
108 94 107 anbi12i 
 |-  ( ( A. r e. { a | E. p e. ( _Left ` A ) a = ( p +s B ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s /\ A. r e. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> ( A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s /\ A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) )
109 81 108 bitri 
 |-  ( A. r e. ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> ( A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s /\ A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) )
110 49 80 109 sylanbrc 
 |-  ( ph -> A. r e. ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s )
111 1 3 cofcutr2d 
 |-  ( ph -> A. e e. ( _Right ` A ) E. r e. R r <_s e )
112 ssltss2 
 |-  ( L < R C_ No )
113 1 112 syl 
 |-  ( ph -> R C_ No )
114 113 adantr 
 |-  ( ( ph /\ e e. ( _Right ` A ) ) -> R C_ No )
115 114 sselda 
 |-  ( ( ( ph /\ e e. ( _Right ` A ) ) /\ r e. R ) -> r e. No )
116 rightssno 
 |-  ( _Right ` A ) C_ No
117 116 sseli 
 |-  ( e e. ( _Right ` A ) -> e e. No )
118 117 ad2antlr 
 |-  ( ( ( ph /\ e e. ( _Right ` A ) ) /\ r e. R ) -> e e. No )
119 8 ad2antrr 
 |-  ( ( ( ph /\ e e. ( _Right ` A ) ) /\ r e. R ) -> B e. No )
120 115 118 119 sleadd1d 
 |-  ( ( ( ph /\ e e. ( _Right ` A ) ) /\ r e. R ) -> ( r <_s e <-> ( r +s B ) <_s ( e +s B ) ) )
121 120 rexbidva 
 |-  ( ( ph /\ e e. ( _Right ` A ) ) -> ( E. r e. R r <_s e <-> E. r e. R ( r +s B ) <_s ( e +s B ) ) )
122 121 ralbidva 
 |-  ( ph -> ( A. e e. ( _Right ` A ) E. r e. R r <_s e <-> A. e e. ( _Right ` A ) E. r e. R ( r +s B ) <_s ( e +s B ) ) )
123 111 122 mpbid 
 |-  ( ph -> A. e e. ( _Right ` A ) E. r e. R ( r +s B ) <_s ( e +s B ) )
124 eqeq1 
 |-  ( w = b -> ( w = ( r +s B ) <-> b = ( r +s B ) ) )
125 124 rexbidv 
 |-  ( w = b -> ( E. r e. R w = ( r +s B ) <-> E. r e. R b = ( r +s B ) ) )
126 125 rexab 
 |-  ( E. b e. { w | E. r e. R w = ( r +s B ) } b <_s ( e +s B ) <-> E. b ( E. r e. R b = ( r +s B ) /\ b <_s ( e +s B ) ) )
127 rexcom4 
 |-  ( E. r e. R E. b ( b = ( r +s B ) /\ b <_s ( e +s B ) ) <-> E. b E. r e. R ( b = ( r +s B ) /\ b <_s ( e +s B ) ) )
128 ovex 
 |-  ( r +s B ) e. _V
129 breq1 
 |-  ( b = ( r +s B ) -> ( b <_s ( e +s B ) <-> ( r +s B ) <_s ( e +s B ) ) )
130 128 129 ceqsexv 
 |-  ( E. b ( b = ( r +s B ) /\ b <_s ( e +s B ) ) <-> ( r +s B ) <_s ( e +s B ) )
131 130 rexbii 
 |-  ( E. r e. R E. b ( b = ( r +s B ) /\ b <_s ( e +s B ) ) <-> E. r e. R ( r +s B ) <_s ( e +s B ) )
132 r19.41v 
 |-  ( E. r e. R ( b = ( r +s B ) /\ b <_s ( e +s B ) ) <-> ( E. r e. R b = ( r +s B ) /\ b <_s ( e +s B ) ) )
133 132 exbii 
 |-  ( E. b E. r e. R ( b = ( r +s B ) /\ b <_s ( e +s B ) ) <-> E. b ( E. r e. R b = ( r +s B ) /\ b <_s ( e +s B ) ) )
134 127 131 133 3bitr3ri 
 |-  ( E. b ( E. r e. R b = ( r +s B ) /\ b <_s ( e +s B ) ) <-> E. r e. R ( r +s B ) <_s ( e +s B ) )
135 126 134 bitri 
 |-  ( E. b e. { w | E. r e. R w = ( r +s B ) } b <_s ( e +s B ) <-> E. r e. R ( r +s B ) <_s ( e +s B ) )
136 ssun1 
 |-  { w | E. r e. R w = ( r +s B ) } C_ ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } )
137 ssrexv 
 |-  ( { w | E. r e. R w = ( r +s B ) } C_ ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) -> ( E. b e. { w | E. r e. R w = ( r +s B ) } b <_s ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) ) )
138 136 137 ax-mp 
 |-  ( E. b e. { w | E. r e. R w = ( r +s B ) } b <_s ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) )
139 135 138 sylbir 
 |-  ( E. r e. R ( r +s B ) <_s ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) )
140 139 ralimi 
 |-  ( A. e e. ( _Right ` A ) E. r e. R ( r +s B ) <_s ( e +s B ) -> A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) )
141 123 140 syl 
 |-  ( ph -> A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) )
142 2 4 cofcutr2d 
 |-  ( ph -> A. f e. ( _Right ` B ) E. s e. S s <_s f )
143 ssltss2 
 |-  ( M < S C_ No )
144 2 143 syl 
 |-  ( ph -> S C_ No )
145 144 adantr 
 |-  ( ( ph /\ f e. ( _Right ` B ) ) -> S C_ No )
146 145 sselda 
 |-  ( ( ( ph /\ f e. ( _Right ` B ) ) /\ s e. S ) -> s e. No )
147 rightssno 
 |-  ( _Right ` B ) C_ No
148 147 sseli 
 |-  ( f e. ( _Right ` B ) -> f e. No )
149 148 ad2antlr 
 |-  ( ( ( ph /\ f e. ( _Right ` B ) ) /\ s e. S ) -> f e. No )
150 6 ad2antrr 
 |-  ( ( ( ph /\ f e. ( _Right ` B ) ) /\ s e. S ) -> A e. No )
151 146 149 150 sleadd2d 
 |-  ( ( ( ph /\ f e. ( _Right ` B ) ) /\ s e. S ) -> ( s <_s f <-> ( A +s s ) <_s ( A +s f ) ) )
152 151 rexbidva 
 |-  ( ( ph /\ f e. ( _Right ` B ) ) -> ( E. s e. S s <_s f <-> E. s e. S ( A +s s ) <_s ( A +s f ) ) )
153 152 ralbidva 
 |-  ( ph -> ( A. f e. ( _Right ` B ) E. s e. S s <_s f <-> A. f e. ( _Right ` B ) E. s e. S ( A +s s ) <_s ( A +s f ) ) )
154 142 153 mpbid 
 |-  ( ph -> A. f e. ( _Right ` B ) E. s e. S ( A +s s ) <_s ( A +s f ) )
155 eqeq1 
 |-  ( t = b -> ( t = ( A +s s ) <-> b = ( A +s s ) ) )
156 155 rexbidv 
 |-  ( t = b -> ( E. s e. S t = ( A +s s ) <-> E. s e. S b = ( A +s s ) ) )
157 156 rexab 
 |-  ( E. b e. { t | E. s e. S t = ( A +s s ) } b <_s ( A +s f ) <-> E. b ( E. s e. S b = ( A +s s ) /\ b <_s ( A +s f ) ) )
158 rexcom4 
 |-  ( E. s e. S E. b ( b = ( A +s s ) /\ b <_s ( A +s f ) ) <-> E. b E. s e. S ( b = ( A +s s ) /\ b <_s ( A +s f ) ) )
159 ovex 
 |-  ( A +s s ) e. _V
160 breq1 
 |-  ( b = ( A +s s ) -> ( b <_s ( A +s f ) <-> ( A +s s ) <_s ( A +s f ) ) )
161 159 160 ceqsexv 
 |-  ( E. b ( b = ( A +s s ) /\ b <_s ( A +s f ) ) <-> ( A +s s ) <_s ( A +s f ) )
162 161 rexbii 
 |-  ( E. s e. S E. b ( b = ( A +s s ) /\ b <_s ( A +s f ) ) <-> E. s e. S ( A +s s ) <_s ( A +s f ) )
163 r19.41v 
 |-  ( E. s e. S ( b = ( A +s s ) /\ b <_s ( A +s f ) ) <-> ( E. s e. S b = ( A +s s ) /\ b <_s ( A +s f ) ) )
164 163 exbii 
 |-  ( E. b E. s e. S ( b = ( A +s s ) /\ b <_s ( A +s f ) ) <-> E. b ( E. s e. S b = ( A +s s ) /\ b <_s ( A +s f ) ) )
165 158 162 164 3bitr3ri 
 |-  ( E. b ( E. s e. S b = ( A +s s ) /\ b <_s ( A +s f ) ) <-> E. s e. S ( A +s s ) <_s ( A +s f ) )
166 157 165 bitri 
 |-  ( E. b e. { t | E. s e. S t = ( A +s s ) } b <_s ( A +s f ) <-> E. s e. S ( A +s s ) <_s ( A +s f ) )
167 ssun2 
 |-  { t | E. s e. S t = ( A +s s ) } C_ ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } )
168 ssrexv 
 |-  ( { t | E. s e. S t = ( A +s s ) } C_ ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) -> ( E. b e. { t | E. s e. S t = ( A +s s ) } b <_s ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) )
169 167 168 ax-mp 
 |-  ( E. b e. { t | E. s e. S t = ( A +s s ) } b <_s ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) )
170 166 169 sylbir 
 |-  ( E. s e. S ( A +s s ) <_s ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) )
171 170 ralimi 
 |-  ( A. f e. ( _Right ` B ) E. s e. S ( A +s s ) <_s ( A +s f ) -> A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) )
172 154 171 syl 
 |-  ( ph -> A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) )
173 ralunb 
 |-  ( A. a e. ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> ( A. a e. { c | E. e e. ( _Right ` A ) c = ( e +s B ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a /\ A. a e. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) )
174 eqeq1 
 |-  ( c = a -> ( c = ( e +s B ) <-> a = ( e +s B ) ) )
175 174 rexbidv 
 |-  ( c = a -> ( E. e e. ( _Right ` A ) c = ( e +s B ) <-> E. e e. ( _Right ` A ) a = ( e +s B ) ) )
176 175 ralab 
 |-  ( A. a e. { c | E. e e. ( _Right ` A ) c = ( e +s B ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> A. a ( E. e e. ( _Right ` A ) a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) )
177 ralcom4 
 |-  ( A. e e. ( _Right ` A ) A. a ( a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. a A. e e. ( _Right ` A ) ( a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) )
178 ovex 
 |-  ( e +s B ) e. _V
179 breq2 
 |-  ( a = ( e +s B ) -> ( b <_s a <-> b <_s ( e +s B ) ) )
180 179 rexbidv 
 |-  ( a = ( e +s B ) -> ( E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) ) )
181 178 180 ceqsalv 
 |-  ( A. a ( a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) )
182 181 ralbii 
 |-  ( A. e e. ( _Right ` A ) A. a ( a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) )
183 r19.23v 
 |-  ( A. e e. ( _Right ` A ) ( a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> ( E. e e. ( _Right ` A ) a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) )
184 183 albii 
 |-  ( A. a A. e e. ( _Right ` A ) ( a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. a ( E. e e. ( _Right ` A ) a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) )
185 177 182 184 3bitr3ri 
 |-  ( A. a ( E. e e. ( _Right ` A ) a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) )
186 176 185 bitri 
 |-  ( A. a e. { c | E. e e. ( _Right ` A ) c = ( e +s B ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) )
187 eqeq1 
 |-  ( d = a -> ( d = ( A +s f ) <-> a = ( A +s f ) ) )
188 187 rexbidv 
 |-  ( d = a -> ( E. f e. ( _Right ` B ) d = ( A +s f ) <-> E. f e. ( _Right ` B ) a = ( A +s f ) ) )
189 188 ralab 
 |-  ( A. a e. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> A. a ( E. f e. ( _Right ` B ) a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) )
190 ralcom4 
 |-  ( A. f e. ( _Right ` B ) A. a ( a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. a A. f e. ( _Right ` B ) ( a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) )
191 ovex 
 |-  ( A +s f ) e. _V
192 breq2 
 |-  ( a = ( A +s f ) -> ( b <_s a <-> b <_s ( A +s f ) ) )
193 192 rexbidv 
 |-  ( a = ( A +s f ) -> ( E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) )
194 191 193 ceqsalv 
 |-  ( A. a ( a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) )
195 194 ralbii 
 |-  ( A. f e. ( _Right ` B ) A. a ( a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) )
196 r19.23v 
 |-  ( A. f e. ( _Right ` B ) ( a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> ( E. f e. ( _Right ` B ) a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) )
197 196 albii 
 |-  ( A. a A. f e. ( _Right ` B ) ( a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. a ( E. f e. ( _Right ` B ) a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) )
198 190 195 197 3bitr3ri 
 |-  ( A. a ( E. f e. ( _Right ` B ) a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) )
199 189 198 bitri 
 |-  ( A. a e. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) )
200 186 199 anbi12i 
 |-  ( ( A. a e. { c | E. e e. ( _Right ` A ) c = ( e +s B ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a /\ A. a e. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> ( A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) /\ A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) )
201 173 200 bitri 
 |-  ( A. a e. ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> ( A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) /\ A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) )
202 141 172 201 sylanbrc 
 |-  ( ph -> A. a e. ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a )
203 eqid 
 |-  ( l e. L |-> ( l +s B ) ) = ( l e. L |-> ( l +s B ) )
204 203 rnmpt 
 |-  ran ( l e. L |-> ( l +s B ) ) = { y | E. l e. L y = ( l +s B ) }
205 ssltex1 
 |-  ( L < L e. _V )
206 1 205 syl 
 |-  ( ph -> L e. _V )
207 206 mptexd 
 |-  ( ph -> ( l e. L |-> ( l +s B ) ) e. _V )
208 rnexg 
 |-  ( ( l e. L |-> ( l +s B ) ) e. _V -> ran ( l e. L |-> ( l +s B ) ) e. _V )
209 207 208 syl 
 |-  ( ph -> ran ( l e. L |-> ( l +s B ) ) e. _V )
210 204 209 eqeltrrid 
 |-  ( ph -> { y | E. l e. L y = ( l +s B ) } e. _V )
211 eqid 
 |-  ( m e. M |-> ( A +s m ) ) = ( m e. M |-> ( A +s m ) )
212 211 rnmpt 
 |-  ran ( m e. M |-> ( A +s m ) ) = { z | E. m e. M z = ( A +s m ) }
213 ssltex1 
 |-  ( M < M e. _V )
214 2 213 syl 
 |-  ( ph -> M e. _V )
215 214 mptexd 
 |-  ( ph -> ( m e. M |-> ( A +s m ) ) e. _V )
216 rnexg 
 |-  ( ( m e. M |-> ( A +s m ) ) e. _V -> ran ( m e. M |-> ( A +s m ) ) e. _V )
217 215 216 syl 
 |-  ( ph -> ran ( m e. M |-> ( A +s m ) ) e. _V )
218 212 217 eqeltrrid 
 |-  ( ph -> { z | E. m e. M z = ( A +s m ) } e. _V )
219 210 218 unexd 
 |-  ( ph -> ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) e. _V )
220 snex 
 |-  { ( A +s B ) } e. _V
221 220 a1i 
 |-  ( ph -> { ( A +s B ) } e. _V )
222 24 sselda 
 |-  ( ( ph /\ l e. L ) -> l e. No )
223 8 adantr 
 |-  ( ( ph /\ l e. L ) -> B e. No )
224 222 223 addscld 
 |-  ( ( ph /\ l e. L ) -> ( l +s B ) e. No )
225 eleq1 
 |-  ( y = ( l +s B ) -> ( y e. No <-> ( l +s B ) e. No ) )
226 224 225 syl5ibrcom 
 |-  ( ( ph /\ l e. L ) -> ( y = ( l +s B ) -> y e. No ) )
227 226 rexlimdva 
 |-  ( ph -> ( E. l e. L y = ( l +s B ) -> y e. No ) )
228 227 abssdv 
 |-  ( ph -> { y | E. l e. L y = ( l +s B ) } C_ No )
229 6 adantr 
 |-  ( ( ph /\ m e. M ) -> A e. No )
230 55 sselda 
 |-  ( ( ph /\ m e. M ) -> m e. No )
231 229 230 addscld 
 |-  ( ( ph /\ m e. M ) -> ( A +s m ) e. No )
232 eleq1 
 |-  ( z = ( A +s m ) -> ( z e. No <-> ( A +s m ) e. No ) )
233 231 232 syl5ibrcom 
 |-  ( ( ph /\ m e. M ) -> ( z = ( A +s m ) -> z e. No ) )
234 233 rexlimdva 
 |-  ( ph -> ( E. m e. M z = ( A +s m ) -> z e. No ) )
235 234 abssdv 
 |-  ( ph -> { z | E. m e. M z = ( A +s m ) } C_ No )
236 228 235 unssd 
 |-  ( ph -> ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) C_ No )
237 6 8 addscld 
 |-  ( ph -> ( A +s B ) e. No )
238 237 snssd 
 |-  ( ph -> { ( A +s B ) } C_ No )
239 velsn 
 |-  ( b e. { ( A +s B ) } <-> b = ( A +s B ) )
240 elun 
 |-  ( a e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) <-> ( a e. { y | E. l e. L y = ( l +s B ) } \/ a e. { z | E. m e. M z = ( A +s m ) } ) )
241 vex 
 |-  a e. _V
242 eqeq1 
 |-  ( y = a -> ( y = ( l +s B ) <-> a = ( l +s B ) ) )
243 242 rexbidv 
 |-  ( y = a -> ( E. l e. L y = ( l +s B ) <-> E. l e. L a = ( l +s B ) ) )
244 241 243 elab 
 |-  ( a e. { y | E. l e. L y = ( l +s B ) } <-> E. l e. L a = ( l +s B ) )
245 eqeq1 
 |-  ( z = a -> ( z = ( A +s m ) <-> a = ( A +s m ) ) )
246 245 rexbidv 
 |-  ( z = a -> ( E. m e. M z = ( A +s m ) <-> E. m e. M a = ( A +s m ) ) )
247 241 246 elab 
 |-  ( a e. { z | E. m e. M z = ( A +s m ) } <-> E. m e. M a = ( A +s m ) )
248 244 247 orbi12i 
 |-  ( ( a e. { y | E. l e. L y = ( l +s B ) } \/ a e. { z | E. m e. M z = ( A +s m ) } ) <-> ( E. l e. L a = ( l +s B ) \/ E. m e. M a = ( A +s m ) ) )
249 240 248 bitri 
 |-  ( a e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) <-> ( E. l e. L a = ( l +s B ) \/ E. m e. M a = ( A +s m ) ) )
250 scutcut 
 |-  ( L < ( ( L |s R ) e. No /\ L <
251 1 250 syl 
 |-  ( ph -> ( ( L |s R ) e. No /\ L <
252 251 simp2d 
 |-  ( ph -> L <
253 252 adantr 
 |-  ( ( ph /\ l e. L ) -> L <
254 simpr 
 |-  ( ( ph /\ l e. L ) -> l e. L )
255 ovex 
 |-  ( L |s R ) e. _V
256 255 snid 
 |-  ( L |s R ) e. { ( L |s R ) }
257 256 a1i 
 |-  ( ( ph /\ l e. L ) -> ( L |s R ) e. { ( L |s R ) } )
258 253 254 257 ssltsepcd 
 |-  ( ( ph /\ l e. L ) -> l
259 3 adantr 
 |-  ( ( ph /\ l e. L ) -> A = ( L |s R ) )
260 258 259 breqtrrd 
 |-  ( ( ph /\ l e. L ) -> l
261 6 adantr 
 |-  ( ( ph /\ l e. L ) -> A e. No )
262 222 261 223 sltadd1d 
 |-  ( ( ph /\ l e. L ) -> ( l  ( l +s B )
263 260 262 mpbid 
 |-  ( ( ph /\ l e. L ) -> ( l +s B )
264 breq1 
 |-  ( a = ( l +s B ) -> ( a  ( l +s B )
265 263 264 syl5ibrcom 
 |-  ( ( ph /\ l e. L ) -> ( a = ( l +s B ) -> a
266 265 rexlimdva 
 |-  ( ph -> ( E. l e. L a = ( l +s B ) -> a
267 scutcut 
 |-  ( M < ( ( M |s S ) e. No /\ M <
268 2 267 syl 
 |-  ( ph -> ( ( M |s S ) e. No /\ M <
269 268 simp2d 
 |-  ( ph -> M <
270 269 adantr 
 |-  ( ( ph /\ m e. M ) -> M <
271 simpr 
 |-  ( ( ph /\ m e. M ) -> m e. M )
272 ovex 
 |-  ( M |s S ) e. _V
273 272 snid 
 |-  ( M |s S ) e. { ( M |s S ) }
274 273 a1i 
 |-  ( ( ph /\ m e. M ) -> ( M |s S ) e. { ( M |s S ) } )
275 270 271 274 ssltsepcd 
 |-  ( ( ph /\ m e. M ) -> m
276 4 adantr 
 |-  ( ( ph /\ m e. M ) -> B = ( M |s S ) )
277 275 276 breqtrrd 
 |-  ( ( ph /\ m e. M ) -> m
278 8 adantr 
 |-  ( ( ph /\ m e. M ) -> B e. No )
279 230 278 229 sltadd2d 
 |-  ( ( ph /\ m e. M ) -> ( m  ( A +s m )
280 277 279 mpbid 
 |-  ( ( ph /\ m e. M ) -> ( A +s m )
281 breq1 
 |-  ( a = ( A +s m ) -> ( a  ( A +s m )
282 280 281 syl5ibrcom 
 |-  ( ( ph /\ m e. M ) -> ( a = ( A +s m ) -> a
283 282 rexlimdva 
 |-  ( ph -> ( E. m e. M a = ( A +s m ) -> a
284 266 283 jaod 
 |-  ( ph -> ( ( E. l e. L a = ( l +s B ) \/ E. m e. M a = ( A +s m ) ) -> a
285 249 284 biimtrid 
 |-  ( ph -> ( a e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) -> a
286 285 imp 
 |-  ( ( ph /\ a e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ) -> a
287 breq2 
 |-  ( b = ( A +s B ) -> ( a  a
288 286 287 syl5ibrcom 
 |-  ( ( ph /\ a e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ) -> ( b = ( A +s B ) -> a
289 239 288 biimtrid 
 |-  ( ( ph /\ a e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ) -> ( b e. { ( A +s B ) } -> a
290 289 3impia 
 |-  ( ( ph /\ a e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) /\ b e. { ( A +s B ) } ) -> a
291 219 221 236 238 290 ssltd 
 |-  ( ph -> ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) <
292 10 sneqd 
 |-  ( ph -> { ( A +s B ) } = { ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) |s ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) ) } )
293 291 292 breqtrd 
 |-  ( ph -> ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) <
294 eqid 
 |-  ( r e. R |-> ( r +s B ) ) = ( r e. R |-> ( r +s B ) )
295 294 rnmpt 
 |-  ran ( r e. R |-> ( r +s B ) ) = { w | E. r e. R w = ( r +s B ) }
296 ssltex2 
 |-  ( L < R e. _V )
297 1 296 syl 
 |-  ( ph -> R e. _V )
298 297 mptexd 
 |-  ( ph -> ( r e. R |-> ( r +s B ) ) e. _V )
299 rnexg 
 |-  ( ( r e. R |-> ( r +s B ) ) e. _V -> ran ( r e. R |-> ( r +s B ) ) e. _V )
300 298 299 syl 
 |-  ( ph -> ran ( r e. R |-> ( r +s B ) ) e. _V )
301 295 300 eqeltrrid 
 |-  ( ph -> { w | E. r e. R w = ( r +s B ) } e. _V )
302 eqid 
 |-  ( s e. S |-> ( A +s s ) ) = ( s e. S |-> ( A +s s ) )
303 302 rnmpt 
 |-  ran ( s e. S |-> ( A +s s ) ) = { t | E. s e. S t = ( A +s s ) }
304 ssltex2 
 |-  ( M < S e. _V )
305 2 304 syl 
 |-  ( ph -> S e. _V )
306 305 mptexd 
 |-  ( ph -> ( s e. S |-> ( A +s s ) ) e. _V )
307 rnexg 
 |-  ( ( s e. S |-> ( A +s s ) ) e. _V -> ran ( s e. S |-> ( A +s s ) ) e. _V )
308 306 307 syl 
 |-  ( ph -> ran ( s e. S |-> ( A +s s ) ) e. _V )
309 303 308 eqeltrrid 
 |-  ( ph -> { t | E. s e. S t = ( A +s s ) } e. _V )
310 301 309 unexd 
 |-  ( ph -> ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) e. _V )
311 113 sselda 
 |-  ( ( ph /\ r e. R ) -> r e. No )
312 8 adantr 
 |-  ( ( ph /\ r e. R ) -> B e. No )
313 311 312 addscld 
 |-  ( ( ph /\ r e. R ) -> ( r +s B ) e. No )
314 eleq1 
 |-  ( w = ( r +s B ) -> ( w e. No <-> ( r +s B ) e. No ) )
315 313 314 syl5ibrcom 
 |-  ( ( ph /\ r e. R ) -> ( w = ( r +s B ) -> w e. No ) )
316 315 rexlimdva 
 |-  ( ph -> ( E. r e. R w = ( r +s B ) -> w e. No ) )
317 316 abssdv 
 |-  ( ph -> { w | E. r e. R w = ( r +s B ) } C_ No )
318 6 adantr 
 |-  ( ( ph /\ s e. S ) -> A e. No )
319 144 sselda 
 |-  ( ( ph /\ s e. S ) -> s e. No )
320 318 319 addscld 
 |-  ( ( ph /\ s e. S ) -> ( A +s s ) e. No )
321 eleq1 
 |-  ( t = ( A +s s ) -> ( t e. No <-> ( A +s s ) e. No ) )
322 320 321 syl5ibrcom 
 |-  ( ( ph /\ s e. S ) -> ( t = ( A +s s ) -> t e. No ) )
323 322 rexlimdva 
 |-  ( ph -> ( E. s e. S t = ( A +s s ) -> t e. No ) )
324 323 abssdv 
 |-  ( ph -> { t | E. s e. S t = ( A +s s ) } C_ No )
325 317 324 unssd 
 |-  ( ph -> ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) C_ No )
326 velsn 
 |-  ( a e. { ( A +s B ) } <-> a = ( A +s B ) )
327 elun 
 |-  ( b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) <-> ( b e. { w | E. r e. R w = ( r +s B ) } \/ b e. { t | E. s e. S t = ( A +s s ) } ) )
328 vex 
 |-  b e. _V
329 328 125 elab 
 |-  ( b e. { w | E. r e. R w = ( r +s B ) } <-> E. r e. R b = ( r +s B ) )
330 328 156 elab 
 |-  ( b e. { t | E. s e. S t = ( A +s s ) } <-> E. s e. S b = ( A +s s ) )
331 329 330 orbi12i 
 |-  ( ( b e. { w | E. r e. R w = ( r +s B ) } \/ b e. { t | E. s e. S t = ( A +s s ) } ) <-> ( E. r e. R b = ( r +s B ) \/ E. s e. S b = ( A +s s ) ) )
332 327 331 bitri 
 |-  ( b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) <-> ( E. r e. R b = ( r +s B ) \/ E. s e. S b = ( A +s s ) ) )
333 3 adantr 
 |-  ( ( ph /\ r e. R ) -> A = ( L |s R ) )
334 251 simp3d 
 |-  ( ph -> { ( L |s R ) } <
335 334 adantr 
 |-  ( ( ph /\ r e. R ) -> { ( L |s R ) } <
336 256 a1i 
 |-  ( ( ph /\ r e. R ) -> ( L |s R ) e. { ( L |s R ) } )
337 simpr 
 |-  ( ( ph /\ r e. R ) -> r e. R )
338 335 336 337 ssltsepcd 
 |-  ( ( ph /\ r e. R ) -> ( L |s R )
339 333 338 eqbrtrd 
 |-  ( ( ph /\ r e. R ) -> A
340 6 adantr 
 |-  ( ( ph /\ r e. R ) -> A e. No )
341 340 311 312 sltadd1d 
 |-  ( ( ph /\ r e. R ) -> ( A  ( A +s B )
342 339 341 mpbid 
 |-  ( ( ph /\ r e. R ) -> ( A +s B )
343 breq2 
 |-  ( b = ( r +s B ) -> ( ( A +s B )  ( A +s B )
344 342 343 syl5ibrcom 
 |-  ( ( ph /\ r e. R ) -> ( b = ( r +s B ) -> ( A +s B )
345 344 rexlimdva 
 |-  ( ph -> ( E. r e. R b = ( r +s B ) -> ( A +s B )
346 4 adantr 
 |-  ( ( ph /\ s e. S ) -> B = ( M |s S ) )
347 268 simp3d 
 |-  ( ph -> { ( M |s S ) } <
348 347 adantr 
 |-  ( ( ph /\ s e. S ) -> { ( M |s S ) } <
349 273 a1i 
 |-  ( ( ph /\ s e. S ) -> ( M |s S ) e. { ( M |s S ) } )
350 simpr 
 |-  ( ( ph /\ s e. S ) -> s e. S )
351 348 349 350 ssltsepcd 
 |-  ( ( ph /\ s e. S ) -> ( M |s S )
352 346 351 eqbrtrd 
 |-  ( ( ph /\ s e. S ) -> B
353 8 adantr 
 |-  ( ( ph /\ s e. S ) -> B e. No )
354 353 319 318 sltadd2d 
 |-  ( ( ph /\ s e. S ) -> ( B  ( A +s B )
355 352 354 mpbid 
 |-  ( ( ph /\ s e. S ) -> ( A +s B )
356 breq2 
 |-  ( b = ( A +s s ) -> ( ( A +s B )  ( A +s B )
357 355 356 syl5ibrcom 
 |-  ( ( ph /\ s e. S ) -> ( b = ( A +s s ) -> ( A +s B )
358 357 rexlimdva 
 |-  ( ph -> ( E. s e. S b = ( A +s s ) -> ( A +s B )
359 345 358 jaod 
 |-  ( ph -> ( ( E. r e. R b = ( r +s B ) \/ E. s e. S b = ( A +s s ) ) -> ( A +s B )
360 332 359 biimtrid 
 |-  ( ph -> ( b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) -> ( A +s B )
361 360 imp 
 |-  ( ( ph /\ b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) ) -> ( A +s B )
362 breq1 
 |-  ( a = ( A +s B ) -> ( a  ( A +s B )
363 361 362 syl5ibrcom 
 |-  ( ( ph /\ b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) ) -> ( a = ( A +s B ) -> a
364 363 ex 
 |-  ( ph -> ( b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) -> ( a = ( A +s B ) -> a
365 364 com23 
 |-  ( ph -> ( a = ( A +s B ) -> ( b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) -> a
366 326 365 biimtrid 
 |-  ( ph -> ( a e. { ( A +s B ) } -> ( b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) -> a
367 366 3imp 
 |-  ( ( ph /\ a e. { ( A +s B ) } /\ b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) ) -> a
368 221 310 238 325 367 ssltd 
 |-  ( ph -> { ( A +s B ) } <
369 292 368 eqbrtrrd 
 |-  ( ph -> { ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) |s ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) ) } <
370 18 110 202 293 369 cofcut1d 
 |-  ( ph -> ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) |s ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) ) = ( ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) |s ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) ) )
371 10 370 eqtrd 
 |-  ( ph -> ( A +s B ) = ( ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) |s ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) ) )